Commit 2025-01-31 16:21 c02933f6

View on Github →

feat(Order/CompleteBooleanAlgebra): Himp in terms of sSup (#20328)

Estimated changes

Modified Mathlib/Order/Bounds/Basic.lean

added theorem isGreatest_compl

added theorem isGreatest_himp

added theorem isLeast_hnot

added theorem isLeast_sdiff

Modified Mathlib/Order/CompleteBooleanAlgebra.lean

added theorem Order.Frame.MinimalAxioms.Order.Coframe.MinimalAxioms.CompleteDistribLattice.MinimalAxioms.CompletelyDistribLattice.MinimalAxioms.compl_eq_sSup_disjoint

added theorem Order.Frame.MinimalAxioms.Order.Coframe.MinimalAxioms.CompleteDistribLattice.MinimalAxioms.CompletelyDistribLattice.MinimalAxioms.himp_eq_sSup

added theorem Order.Frame.MinimalAxioms.Order.Coframe.MinimalAxioms.CompleteDistribLattice.MinimalAxioms.CompletelyDistribLattice.MinimalAxioms.hnot_eq_sInf_codisjoint

added theorem Order.Frame.MinimalAxioms.Order.Coframe.MinimalAxioms.CompleteDistribLattice.MinimalAxioms.CompletelyDistribLattice.MinimalAxioms.sdiff_eq_sInf