Commit 2025-02-05 05:32 803e276b

View on Github →

refactor(Order/CompleteBooleanAlgebra): a complete lattice which is a Heyting algebra is automatically a frame (#21391) Every complete lattice that is a heyting algebra is also a frame. This is because the Heyting implication is the right adjoint to ⊓, which means that ⊓ now preserves infinite suprema (because it is a left adjoint).

Estimated changes

Modified Mathlib/Data/Fintype/Order.lean

Modified Mathlib/Order/CompleteBooleanAlgebra.lean

deleted theorem Order.Frame.MinimalAxioms.Order.Coframe.MinimalAxioms.CompleteDistribLattice.MinimalAxioms.CompletelyDistribLattice.MinimalAxioms.inf_sSup_eq

deleted theorem Order.Frame.MinimalAxioms.Order.Coframe.MinimalAxioms.CompleteDistribLattice.MinimalAxioms.CompletelyDistribLattice.MinimalAxioms.sup_sInf_eq

modified def Order.Frame.MinimalAxioms.Order.Coframe.MinimalAxioms.CompleteDistribLattice.MinimalAxioms.of

modified def Order.Frame.MinimalAxioms.Order.Coframe.MinimalAxioms.of

modified def Order.Frame.MinimalAxioms.of

added theorem inf_sSup_eq

added theorem sup_sInf_eq

Modified Mathlib/Order/Copy.lean

Modified Mathlib/Order/Heyting/Basic.lean

added theorem gc_inf_himp

added theorem gc_sdiff_sup