Commit 2023-09-04 13:18 57559c59

View on Github →

feat: Sup-closed sets (#6901) This defines sets closed under supremum/infimum, shows that every set has a sup-closure/inf-closure and prove that if every sup-closed/inf-closed set in a sup-semilattice/inf-semilattice has a least upper bound/greatest lower, then the lattice is in fact complete. As a bonus, we use our new predicate in Order.CompactlyGenerated.

Estimated changes

modified theorem Convex.convexHull_eq
added theorem Finset.inf'_union
added theorem Finset.sup'_union
added theorem InfClosed.codirectedOn
added theorem InfClosed.inter
added def InfClosed
added theorem SupClosed.directedOn
added theorem SupClosed.inter
added def SupClosed
added theorem infClosed_empty
added theorem infClosed_iInter
added theorem infClosed_infClosure
added theorem infClosed_sInter
added theorem infClosed_singleton
added theorem infClosed_univ
added def infClosure
added theorem infClosure_empty
added theorem infClosure_eq_self
added theorem infClosure_idem
added theorem infClosure_mono
added theorem infClosure_singleton
added theorem infClosure_univ
added theorem isGLB_infClosure
added theorem isLUB_supClosure
added theorem lowerBounds_infClosure
added theorem subset_infClosure
added theorem subset_supClosure
added theorem supClosed_empty
added theorem supClosed_iInter
added theorem supClosed_sInter
added theorem supClosed_singleton
added theorem supClosed_supClosure
added theorem supClosed_univ
added def supClosure
added theorem supClosure_empty
added theorem supClosure_eq_self
added theorem supClosure_idem
added theorem supClosure_mono
added theorem supClosure_singleton
added theorem supClosure_univ
added theorem upperBounds_supClosure