Move ODual to the top of Part 9?

[zwang123]

I suggest moving things from codu to odubas to the beginning of part 9 (potentially making it a new 9.1), and the remaining of “9.2.3 The dual of an ordered set” to (potentially the beginning of) their corresponding sections (poset/meet/join/glb/lub to the poset section; lat to lat section; clat to clat section)

The benefit is multiple (or even significant, tbh):

• Other theorems can make use of ODual (e.g., theorems proved for lub could potentially be reused by glb)
  • A side effect of ODual not being the top of Part 9 is that latmass is weirdly not in the section of lattice but instead at the top of Distributive lattices
• Things are more organized: for example, poslubmo should be in the poset section IMO

I confirmed that these theorems (codu to odubas) have no dependency on any theorems in part 9 so it should be safe to move.

P.S. The toset part worth a new section IMO especially after me moving some of TA's theorems to main.

[avekens]

I fully agree with @zwang123's proposal. This would result in a clearer and more comprehensible structure. And it could help to shorten proofs, as indicated by the "editorial" in the comment of ~df-odu.

The definition of Toset and the related theorems could be moved into a new section 9.2.2 (the current section 9.2.2 Lattices becomes 9.2.3).

[benjub]

I agree. The new TOC could be:

9.  Order theory
9.1.  Dual of an order structure
9.2.  Preordered sets
9.2.  Directed sets
9.3.  Partially ordered sets
9.4.  Totally ordered sets
9.5.  Lattices
9.5.1.  Lattices
9.5.2.  Distributive lattices
9.5.3.  The distributive lattice of sets under inclusion
9.6.  Posets, directed sets, and lattices as relations
        (This treatment predates our systematic use of extensible structures;
         TODO: see to what extent we keep it, merge it, update it to use the
         extensible structures framework.)

[avekens]

Aftrer #4298 was merged, I had a look at the HTML pages. Here my remarks:

• in many comments, "poset" is mentioned, but not occuring ih the theorem (e.g., ~lubfval: "Value of the least upper bound function of a poset.") can it be removed ("Value of the least upper bound function.")?
• LUB should be expanded to "least upper bound" or "least upper bound function". The same for GLB.
• Comment of ~glbcl is wrong: "The least upper bound function value belongs to the base set." -> "The greatest lower bound function value belongs to the base set."
• 0. and 1. (currently in subsection 9.4 "Totally ordered sets (tosets)") should be moved to subsection 9.3 "Partially ordered sets (posets)".
• There are several TODOs in this part left: ~joinfval, ~joinval2lem, ~meetfval, ~meetval2lem, ~clatl, ~meet0/join0, ~mreclat(BAD), ~df-ipo
• Since the" commented-out notes for lattices as relations." are not visible on the HTML pages, this section header comment should be enhanced, e.g.: "Lattices as relations are not defined yet. See commented-out notes for lattices as relations.". See, however, also #4302.
• The subsection title "Directed sets, nets" should be changed to "Directed sets as relation" ("nets" are nowhere defined/mentioned!).

[avekens]

Finally, which proofs will benefit from the availability of ODual now? Are there already some applications? Since this was the original motivation for the new structure, (at least some) applications of it should be provided (maybe "the theorems proved for lub could potentially be reused by glb", as mentioned above), before this issue is closed.

[zwang123]

An immediate benefit is to move the first few theorems in the old distributive lattice section to their right places, the lattice section. (Already done) A quick benefit is to enable moving my theorems to main because some of them depend on dual.