Commit 2024-07-23 12:07 3cd501d4

View on Github →

refactor: Make Frame extend HeytingAlgebra (#10560) It is mathematically true that a frame is a Heyting algebra. However we want nice defeqs, so we can't just provide an instance defining himp as some supremum. Instead, we need Frame to directly extend HeytingAlgebra.

Estimated changes

Modified Archive/Imo/Imo1998Q2.lean

Modified Mathlib/Combinatorics/SimpleGraph/Finsubgraph.lean

added theorem SimpleGraph.Finsubgraph.coe_compl

added theorem SimpleGraph.Finsubgraph.coe_himp

added theorem SimpleGraph.Finsubgraph.coe_hnot

added theorem SimpleGraph.Finsubgraph.coe_sdiff

modified theorem SimpleGraph.Finsubgraph.coe_top

Modified Mathlib/Combinatorics/SimpleGraph/Subgraph.lean

added def SimpleGraph.Subgraph.completelyDistribLatticeMinimalAxioms

Modified Mathlib/Data/Fintype/Order.lean

Modified Mathlib/MeasureTheory/MeasurableSpace/Basic.lean

Modified Mathlib/ModelTheory/Definability.lean

Modified Mathlib/Order/BooleanAlgebra.lean

Modified Mathlib/Order/CompleteBooleanAlgebra.lean

added structure CompleteDistribLattice.MinimalAxioms

added structure CompletelyDistribLattice.MinimalAxioms

added theorem Order.Frame.MinimalAxioms.Order.Coframe.MinimalAxioms.CompleteDistribLattice.MinimalAxioms.CompletelyDistribLattice.MinimalAxioms.PUnit.sInf_eq

added theorem Order.Frame.MinimalAxioms.Order.Coframe.MinimalAxioms.CompleteDistribLattice.MinimalAxioms.CompletelyDistribLattice.MinimalAxioms.PUnit.sSup_eq

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

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

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

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

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

added theorem Order.Frame.MinimalAxioms.Order.Coframe.MinimalAxioms.CompleteDistribLattice.MinimalAxioms.CompletelyDistribLattice.MinimalAxioms.compl_sInf'

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

added theorem Order.Frame.MinimalAxioms.Order.Coframe.MinimalAxioms.CompleteDistribLattice.MinimalAxioms.CompletelyDistribLattice.MinimalAxioms.compl_sSup'

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

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

added theorem Order.Frame.MinimalAxioms.Order.Coframe.MinimalAxioms.CompleteDistribLattice.MinimalAxioms.CompletelyDistribLattice.MinimalAxioms.disjoint_iSup₂_iff

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

added theorem Order.Frame.MinimalAxioms.Order.Coframe.MinimalAxioms.CompleteDistribLattice.MinimalAxioms.CompletelyDistribLattice.MinimalAxioms.iInf_iSup_eq'

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

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

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

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

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

added theorem Order.Frame.MinimalAxioms.Order.Coframe.MinimalAxioms.CompleteDistribLattice.MinimalAxioms.CompletelyDistribLattice.MinimalAxioms.iInf₂_sup_eq

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

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

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

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

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

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

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

added theorem Order.Frame.MinimalAxioms.Order.Coframe.MinimalAxioms.CompleteDistribLattice.MinimalAxioms.CompletelyDistribLattice.MinimalAxioms.iSup₂_disjoint_iff

added theorem Order.Frame.MinimalAxioms.Order.Coframe.MinimalAxioms.CompleteDistribLattice.MinimalAxioms.CompletelyDistribLattice.MinimalAxioms.iSup₂_inf_eq

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

added theorem Order.Frame.MinimalAxioms.Order.Coframe.MinimalAxioms.CompleteDistribLattice.MinimalAxioms.CompletelyDistribLattice.MinimalAxioms.inf_iSup₂_eq

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

added def Order.Frame.MinimalAxioms.Order.Coframe.MinimalAxioms.CompleteDistribLattice.MinimalAxioms.CompletelyDistribLattice.MinimalAxioms.of

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

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

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

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

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

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

added theorem Order.Frame.MinimalAxioms.Order.Coframe.MinimalAxioms.CompleteDistribLattice.MinimalAxioms.CompletelyDistribLattice.MinimalAxioms.sup_iInf₂_eq

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

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

added theorem Order.Frame.MinimalAxioms.Order.Coframe.MinimalAxioms.iInf_sup_eq

added def Order.Frame.MinimalAxioms.Order.Coframe.MinimalAxioms.of

added theorem Order.Frame.MinimalAxioms.Order.Coframe.MinimalAxioms.sInf_sup_eq

added theorem Order.Frame.MinimalAxioms.Order.Coframe.MinimalAxioms.sup_iInf_eq

added theorem Order.Frame.MinimalAxioms.Order.Coframe.MinimalAxioms.sup_iInf₂_eq

added theorem Order.Frame.MinimalAxioms.Order.Coframe.MinimalAxioms.sup_sInf_eq

added theorem Order.Frame.MinimalAxioms.iSup_inf_eq

added theorem Order.Frame.MinimalAxioms.inf_iSup_eq

added theorem Order.Frame.MinimalAxioms.inf_iSup₂_eq

added theorem Order.Frame.MinimalAxioms.inf_sSup_eq

added def Order.Frame.MinimalAxioms.of

added theorem Order.Frame.MinimalAxioms.sSup_inf_eq

deleted theorem PUnit.sInf_eq

deleted theorem PUnit.sSup_eq

deleted theorem biInf_sup_biInf

deleted theorem biSup_inf_biSup

deleted theorem biSup_symmDiff_biSup_le

deleted theorem compl_iInf

deleted theorem compl_iSup

deleted theorem compl_sInf'

deleted theorem compl_sInf

deleted theorem compl_sSup'

deleted theorem compl_sSup

deleted theorem disjoint_iSup_iff

deleted theorem disjoint_iSup₂_iff

deleted theorem disjoint_sSup_iff

deleted theorem iInf_iSup_eq

deleted theorem iInf_sup_eq

deleted theorem iInf_sup_iInf

deleted theorem iInf_sup_of_antitone

deleted theorem iInf_sup_of_monotone

deleted theorem iInf₂_sup_eq

deleted theorem iSup_disjoint_iff

deleted theorem iSup_iInf_eq

modified theorem iSup_iInf_le

deleted theorem iSup_inf_eq

deleted theorem iSup_inf_iSup

deleted theorem iSup_inf_of_antitone

deleted theorem iSup_inf_of_monotone

deleted theorem iSup_symmDiff_iSup_le

deleted theorem iSup₂_disjoint_iff

deleted theorem iSup₂_inf_eq

deleted theorem inf_iSup_eq

deleted theorem inf_iSup₂_eq

deleted theorem inf_sSup_eq

deleted theorem sInf_sup_eq

deleted theorem sInf_sup_sInf

deleted theorem sSup_disjoint_iff

deleted theorem sSup_inf_eq

deleted theorem sSup_inf_sSup

deleted theorem sup_iInf_eq

deleted theorem sup_iInf₂_eq

deleted theorem sup_sInf_eq

Modified Mathlib/Order/CompleteLattice.lean

added theorem iInf_ulift

added theorem iInf_unique

added theorem iSup_ulift

added theorem iSup_unique

Modified Mathlib/Order/Copy.lean

Modified Mathlib/Order/Filter/Basic.lean

added def Filter.coframeMinimalAxioms

Modified Mathlib/Order/UpperLower/Basic.lean

Modified Mathlib/Topology/Sets/Closeds.lean

added def TopologicalSpace.Closeds.coframeMinimalAxioms

Modified Mathlib/Topology/Sets/Compacts.lean

Modified Mathlib/Topology/Sets/Opens.lean

added def TopologicalSpace.Opens.frameMinimalAxioms