Theorem Order.Frame.MinimalAxioms.Order.Coframe.MinimalAxioms.CompleteDistribLattice.MinimalAxioms.CompletelyDistribLattice.MinimalAxioms.iInf_sup_of_antitone
Modification history
2025-12-08 05:19
Mathlib/Order/CompleteBooleanAlgebra.lean
refactor: make `abbrev`s for `IsDirected α (· ≤ ·)` and `IsDirected α (· ≥ ·)` (#32462) …
Modified Order.Frame.MinimalAxioms.Order.Coframe.MinimalAxioms.CompleteDistribLattice.MinimalAxioms.CompletelyDistribLattice.MinimalAxioms.iInf_sup_of_antitoneView on Github →