Restructure part 9 (#4298)

* Move dual to top of part 9 * remove redundant $d for oduglb and odulat * rename: posglbd -> posglbdg * rename: posglbd -> posglbdg (changes-set.txt) * toInc to after dlat; add tosets section * latmass to latdisd -> lattice section * add Complete lattices section * latmass to latdisd -> lattice section (before clat) * add explanations for lattices as relations * reverse order for join0 and meet0 and for odu*, for consistency
metamath · Oct 19, 2024 · 2c23f68 · 2c23f68
1 parent 1987621
commit 2c23f68
Show file tree

Hide file tree

Showing 2 changed files with 539 additions and 508 deletions.
diff --git a/changes-set.txt b/changes-set.txt
@@ -95,6 +95,7 @@ make a github issue.)
 
 DONE:
 Date      Old       New         Notes
+17-Oct-24 posglbd   posglbdg    compare to poslubdg
 15-Oct-24 ---       ---         well-founded induction theorems moved
                                 from SF's mathbox to main set.mm
 12-Oct-24 syl5rbb   bitr2id     compare to bitr2i or bitr2d