[Merged by Bors] - refactor(Order/CompleteBooleanAlgebra): a complete lattice which is a Heyting algebra is automatically a frame by Bergschaf · Pull Request #21391 · leanprover-community/mathlib4

Bergschaf · 2025-02-03T20:56:44Z

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).

So, in my opinion, we don't need the inf_sSup_le_iSup_inf for the Frame structure anymore. I'm not sure if the way I implemented this is optimal, I'm happy to learn how to do this better.

github-actions · 2025-02-03T20:57:41Z

PR summary 42e09d9688

Import changes exceeding 2%

%	File
+21.56%	`Mathlib.Order.Heyting.Basic`

Import changes for modified files

Dependency changes

File	Base Count	Head Count	Change
Mathlib.Order.Heyting.Basic	167	203	+36 (+21.56%)
Mathlib.Order.CompleteBooleanAlgebra	262	265	+3 (+1.15%)

Import changes for all files

Files	Import difference
272 files `Mathlib.Algebra.BigOperators.Group.Finset.Defs` `Mathlib.Algebra.BigOperators.Group.Multiset.Basic` `Mathlib.Algebra.BigOperators.Group.Multiset.Defs` `Mathlib.Algebra.BigOperators.Ring.Multiset` `Mathlib.Algebra.BigOperators.RingEquiv` `Mathlib.Algebra.Category.Grp.Zero` `Mathlib.Algebra.Category.Ring.Colimits` `Mathlib.Algebra.CharP.Basic` `Mathlib.Algebra.CharP.Pi` `Mathlib.Algebra.CharZero.Infinite` `Mathlib.Algebra.FreeMonoid.Symbols` `Mathlib.Algebra.GCDMonoid.Finset` `Mathlib.Algebra.GCDMonoid.Multiset` `Mathlib.Algebra.Group.PNatPowAssoc` `Mathlib.Algebra.IsPrimePow` `Mathlib.Algebra.Order.Algebra` `Mathlib.Algebra.Order.BigOperators.Group.Multiset` `Mathlib.Algebra.Order.BigOperators.GroupWithZero.Multiset` `Mathlib.Algebra.Order.BigOperators.Ring.Multiset` `Mathlib.Algebra.Order.Group.Cone` `Mathlib.Algebra.Order.Group.Multiset` `Mathlib.Algebra.Order.Hom.Ring` `Mathlib.Algebra.Order.Interval.Set.Group` `Mathlib.Algebra.Order.Invertible` `Mathlib.Algebra.Order.Module.Algebra` `Mathlib.Algebra.Order.Module.Defs` `Mathlib.Algebra.Order.Module.OrderedSMul` `Mathlib.Algebra.Order.Monoid.Submonoid` `Mathlib.Algebra.Order.Monovary` `Mathlib.Algebra.Order.Quantale` `Mathlib.Algebra.Order.Ring.Abs` `Mathlib.Algebra.Order.Ring.Cast` `Mathlib.Algebra.Order.Ring.Cone` `Mathlib.Algebra.Order.Ring.Idempotent` `Mathlib.Algebra.Order.Ring.Int` `Mathlib.Algebra.Order.Ring.Nat` `Mathlib.Algebra.Order.Ring.Pow` `Mathlib.Algebra.Regular.Pow` `Mathlib.Algebra.Ring.Subring.Order` `Mathlib.Algebra.Ring.Subsemiring.Order` `Mathlib.Algebra.Star.BigOperators` `Mathlib.CategoryTheory.Action.Basic` `Mathlib.CategoryTheory.Adjunction.Comma` `Mathlib.CategoryTheory.Adjunction.Evaluation` `Mathlib.CategoryTheory.Adjunction.Limits` `Mathlib.CategoryTheory.Adjunction.Over` `Mathlib.CategoryTheory.Adjunction.PartialAdjoint` `Mathlib.CategoryTheory.Bicategory.Kan.Adjunction` `Mathlib.CategoryTheory.Bicategory.Kan.HasKan` `Mathlib.CategoryTheory.Category.Factorisation` `Mathlib.CategoryTheory.Category.Grpd` `Mathlib.CategoryTheory.Category.Pairwise` `Mathlib.CategoryTheory.Comma.LocallySmall` `Mathlib.CategoryTheory.ComposableArrows` `Mathlib.CategoryTheory.Countable` `Mathlib.CategoryTheory.EffectiveEpi.Basic` `Mathlib.CategoryTheory.EffectiveEpi.Comp` `Mathlib.CategoryTheory.EffectiveEpi.Coproduct` `Mathlib.CategoryTheory.EffectiveEpi.Enough` `Mathlib.CategoryTheory.EffectiveEpi.Preserves` `Mathlib.CategoryTheory.EffectiveEpi.RegularEpi` `Mathlib.CategoryTheory.EssentiallySmall` `Mathlib.CategoryTheory.Filtered.Basic` `Mathlib.CategoryTheory.Filtered.Connected` `Mathlib.CategoryTheory.Filtered.Grothendieck` `Mathlib.CategoryTheory.Filtered.Small` `Mathlib.CategoryTheory.FinCategory.AsType` `Mathlib.CategoryTheory.FinCategory.Basic` `Mathlib.CategoryTheory.Functor.KanExtension.Adjunction` `Mathlib.CategoryTheory.Functor.KanExtension.Basic` `Mathlib.CategoryTheory.Functor.KanExtension.Pointwise` `Mathlib.CategoryTheory.Limits.Bicones` `Mathlib.CategoryTheory.Limits.ConeCategory` `Mathlib.CategoryTheory.Limits.Connected` `Mathlib.CategoryTheory.Limits.Constructions.EventuallyConstant` `Mathlib.CategoryTheory.Limits.Constructions.FiniteProductsOfBinaryProducts` `Mathlib.CategoryTheory.Limits.Constructions.Over.Connected` `Mathlib.CategoryTheory.Limits.Constructions.Pullbacks` `Mathlib.CategoryTheory.Limits.Constructions.WeaklyInitial` `Mathlib.CategoryTheory.Limits.Creates` `Mathlib.CategoryTheory.Limits.EssentiallySmall` `Mathlib.CategoryTheory.Limits.ExactFunctor` `Mathlib.CategoryTheory.Limits.Fubini` `Mathlib.CategoryTheory.Limits.FullSubcategory` `Mathlib.CategoryTheory.Limits.FunctorCategory.Basic` `Mathlib.CategoryTheory.Limits.FunctorCategory.Finite` `Mathlib.CategoryTheory.Limits.FunctorCategory.Shapes.Products` `Mathlib.CategoryTheory.Limits.HasLimits` `Mathlib.CategoryTheory.Limits.Pi` `Mathlib.CategoryTheory.Limits.Preorder` `Mathlib.CategoryTheory.Limits.Preserves.Basic` `Mathlib.CategoryTheory.Limits.Preserves.Creates.Finite` `Mathlib.CategoryTheory.Limits.Preserves.Filtered` `Mathlib.CategoryTheory.Limits.Preserves.Finite` `Mathlib.CategoryTheory.Limits.Preserves.Grothendieck` `Mathlib.CategoryTheory.Limits.Preserves.Limits` `Mathlib.CategoryTheory.Limits.Preserves.Shapes.BinaryProducts` `Mathlib.CategoryTheory.Limits.Preserves.Shapes.Equalizers` `Mathlib.CategoryTheory.Limits.Preserves.Shapes.Products` `Mathlib.CategoryTheory.Limits.Preserves.Shapes.Terminal` `Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts` `Mathlib.CategoryTheory.Limits.Shapes.CombinedProducts` `Mathlib.CategoryTheory.Limits.Shapes.Connected` `Mathlib.CategoryTheory.Limits.Shapes.DisjointCoproduct` `Mathlib.CategoryTheory.Limits.Shapes.End` `Mathlib.CategoryTheory.Limits.Shapes.Equalizers` `Mathlib.CategoryTheory.Limits.Shapes.Equivalence` `Mathlib.CategoryTheory.Limits.Shapes.FiniteLimits` `Mathlib.CategoryTheory.Limits.Shapes.FiniteProducts` `Mathlib.CategoryTheory.Limits.Shapes.Grothendieck` `Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer` `Mathlib.CategoryTheory.Limits.Shapes.PiProd` `Mathlib.CategoryTheory.Limits.Shapes.Preorder.Basic` `Mathlib.CategoryTheory.Limits.Shapes.Products` `Mathlib.CategoryTheory.Limits.Shapes.Pullback.Assoc` `Mathlib.CategoryTheory.Limits.Shapes.Pullback.Cospan` `Mathlib.CategoryTheory.Limits.Shapes.Pullback.HasPullback` `Mathlib.CategoryTheory.Limits.Shapes.Pullback.Iso` `Mathlib.CategoryTheory.Limits.Shapes.Pullback.Mono` `Mathlib.CategoryTheory.Limits.Shapes.Pullback.Pasting` `Mathlib.CategoryTheory.Limits.Shapes.Pullback.PullbackCone` `Mathlib.CategoryTheory.Limits.Shapes.RegularMono` `Mathlib.CategoryTheory.Limits.Shapes.SplitCoequalizer` `Mathlib.CategoryTheory.Limits.Shapes.SplitEqualizer` `Mathlib.CategoryTheory.Limits.Shapes.StrictInitial` `Mathlib.CategoryTheory.Limits.Shapes.Terminal` `Mathlib.CategoryTheory.Limits.Shapes.WideEqualizers` `Mathlib.CategoryTheory.Limits.Shapes.WidePullbacks` `Mathlib.CategoryTheory.Limits.Shapes.ZeroObjects` `Mathlib.CategoryTheory.Limits.Unit` `Mathlib.CategoryTheory.Monad.Products` `Mathlib.CategoryTheory.Monoidal.OfChosenFiniteProducts.Basic` `Mathlib.CategoryTheory.SingleObj` `Mathlib.CategoryTheory.SmallObject.Construction` `Mathlib.Computability.Tape` `Mathlib.Control.EquivFunctor.Instances` `Mathlib.Control.Fix` `Mathlib.Control.Functor.Multivariate` `Mathlib.Control.Random` `Mathlib.Data.BitVec` `Mathlib.Data.Bool.Count` `Mathlib.Data.DFinsupp.Defs` `Mathlib.Data.DFinsupp.FiniteInfinite` `Mathlib.Data.DFinsupp.Module` `Mathlib.Data.DFinsupp.NeLocus` `Mathlib.Data.DFinsupp.Order` `Mathlib.Data.DFinsupp.Sigma` `Mathlib.Data.DFinsupp.Small` `Mathlib.Data.Fin.Fin2` `Mathlib.Data.Fin.Parity` `Mathlib.Data.Fin.Tuple.Finset` `Mathlib.Data.FinEnum.Option` `Mathlib.Data.FinEnum` `Mathlib.Data.Finite.Set` `Mathlib.Data.Finite.Sum` `Mathlib.Data.Finset.Attach` `Mathlib.Data.Finset.Basic` `Mathlib.Data.Finset.Card` `Mathlib.Data.Finset.Dedup` `Mathlib.Data.Finset.Defs` `Mathlib.Data.Finset.Disjoint` `Mathlib.Data.Finset.Empty` `Mathlib.Data.Finset.Erase` `Mathlib.Data.Finset.Filter` `Mathlib.Data.Finset.Fin` `Mathlib.Data.Finset.Fold` `Mathlib.Data.Finset.Image` `Mathlib.Data.Finset.Insert` `Mathlib.Data.Finset.Lattice.Basic` `Mathlib.Data.Finset.Lattice.Lemmas` `Mathlib.Data.Finset.Option` `Mathlib.Data.Finset.Order` `Mathlib.Data.Finset.Pi` `Mathlib.Data.Finset.Piecewise` `Mathlib.Data.Finset.Prod` `Mathlib.Data.Finset.Range` `Mathlib.Data.Finset.SDiff` `Mathlib.Data.Finset.Sum` `Mathlib.Data.Finset.SymmDiff` `Mathlib.Data.Finset.Union` `Mathlib.Data.Finset.Update` `Mathlib.Data.Fintype.Basic` `Mathlib.Data.Fintype.Card` `Mathlib.Data.Fintype.Option` `Mathlib.Data.Fintype.Parity` `Mathlib.Data.Fintype.Pi` `Mathlib.Data.Fintype.Prod` `Mathlib.Data.Fintype.Quotient` `Mathlib.Data.Fintype.Shrink` `Mathlib.Data.Fintype.Sum` `Mathlib.Data.Int.LeastGreatest` `Mathlib.Data.Int.Lemmas` `Mathlib.Data.Int.Order.Lemmas` `Mathlib.Data.Int.Order.Units` `Mathlib.Data.Int.Range` `Mathlib.Data.List.EditDistance.Estimator` `Mathlib.Data.List.Iterate` `Mathlib.Data.List.NodupEquivFin` `Mathlib.Data.List.Pi` `Mathlib.Data.List.Sort` `Mathlib.Data.MLList.BestFirst` `Mathlib.Data.Matrix.CharP` `Mathlib.Data.Multiset.Antidiagonal` `Mathlib.Data.Multiset.Basic` `Mathlib.Data.Multiset.Bind` `Mathlib.Data.Multiset.Dedup` `Mathlib.Data.Multiset.DershowitzManna` `Mathlib.Data.Multiset.FinsetOps` `Mathlib.Data.Multiset.Fold` `Mathlib.Data.Multiset.Lattice` `Mathlib.Data.Multiset.NatAntidiagonal` `Mathlib.Data.Multiset.Nodup` `Mathlib.Data.Multiset.OrderedMonoid` `Mathlib.Data.Multiset.Pi` `Mathlib.Data.Multiset.Powerset` `Mathlib.Data.Multiset.Range` `Mathlib.Data.Multiset.Sections` `Mathlib.Data.Multiset.Sort` `Mathlib.Data.Multiset.Sum` `Mathlib.Data.Nat.BitIndices` `Mathlib.Data.Nat.Cast.Order.Ring` `Mathlib.Data.Nat.ChineseRemainder` `Mathlib.Data.Nat.Dist` `Mathlib.Data.Nat.Factors` `Mathlib.Data.Nat.GCD.BigOperators` `Mathlib.Data.Nat.MaxPowDiv` `Mathlib.Data.Nat.Upto` `Mathlib.Data.Num.Lemmas` `Mathlib.Data.PNat.Basic` `Mathlib.Data.PNat.Factors` `Mathlib.Data.PNat.Find` `Mathlib.Data.PNat.Prime` `Mathlib.Data.Rat.Sqrt` `Mathlib.Data.Set.Finite.Basic` `Mathlib.Data.Set.Finite.Range` `Mathlib.Data.Sum.Lattice` `Mathlib.Data.TypeVec` `Mathlib.Data.UInt` `Mathlib.Data.Vector3` `Mathlib.Data.ZMod.Defs` `Mathlib.Order.Booleanisation` `Mathlib.Order.Bounds.OrderIso` `Mathlib.Order.CompleteLattice` `Mathlib.Order.Estimator` `Mathlib.Order.Fin.Basic` `Mathlib.Order.Fin.Finset` `Mathlib.Order.Fin.SuccAboveOrderIso` `Mathlib.Order.Fin.Tuple` `Mathlib.Order.Heyting.Hom` `Mathlib.Order.Hom.Lattice` `Mathlib.Order.Hom.Set` `Mathlib.Order.Interval.Set.Infinite` `Mathlib.Order.Interval.Set.OrderEmbedding` `Mathlib.Order.Interval.Set.OrderIso` `Mathlib.Order.Part` `Mathlib.SetTheory.Lists` `Mathlib.Tactic.FieldSimp` `Mathlib.Tactic.FinCases` `Mathlib.Tactic.Finiteness` `Mathlib.Tactic.GCongr` `Mathlib.Tactic.Linarith.Datatypes` `Mathlib.Tactic.Linarith.Lemmas` `Mathlib.Tactic.Linarith.Oracle.FourierMotzkin` `Mathlib.Tactic.Linarith.Oracle.SimplexAlgorithm` `Mathlib.Tactic.Linarith.Parsing` `Mathlib.Tactic.Linarith.Preprocessing` `Mathlib.Tactic.Linarith.Verification` `Mathlib.Tactic.LinearCombination.Lemmas` `Mathlib.Tactic.Positivity.Core` `Mathlib.Tactic.Qify` `Mathlib.Tactic.Widget.GCongr` `Mathlib.Testing.Plausible.Sampleable`	1
`Mathlib.Order.Category.FinPartOrd`	2
239 files `Mathlib.Algebra.Category.Grp.Preadditive` `Mathlib.Algebra.Category.MonCat.Colimits` `Mathlib.Algebra.Homology.ShortComplex.Basic` `Mathlib.Algebra.Homology.ShortComplex.FunctorEquivalence` `Mathlib.Algebra.Homology.ShortComplex.Homology` `Mathlib.Algebra.Homology.ShortComplex.LeftHomology` `Mathlib.Algebra.Homology.ShortComplex.Limits` `Mathlib.Algebra.Homology.ShortComplex.PreservesHomology` `Mathlib.Algebra.Homology.ShortComplex.QuasiIso` `Mathlib.Algebra.Homology.ShortComplex.Retract` `Mathlib.Algebra.Homology.ShortComplex.RightHomology` `Mathlib.AlgebraicTopology.ModelCategory.Basic` `Mathlib.AlgebraicTopology.ModelCategory.CategoryWithCofibrations` `Mathlib.CategoryTheory.Abelian.Images` `Mathlib.CategoryTheory.Abelian.NonPreadditive` `Mathlib.CategoryTheory.Adjunction.FullyFaithful` `Mathlib.CategoryTheory.Adjunction.Lifting.Left` `Mathlib.CategoryTheory.Adjunction.Lifting.Right` `Mathlib.CategoryTheory.Adjunction.Reflective` `Mathlib.CategoryTheory.Adjunction.Triple` `Mathlib.CategoryTheory.Bicategory.SingleObj` `Mathlib.CategoryTheory.Category.Cat.Limit` `Mathlib.CategoryTheory.ChosenFiniteProducts.Cat` `Mathlib.CategoryTheory.ChosenFiniteProducts.FunctorCategory` `Mathlib.CategoryTheory.ChosenFiniteProducts.InfSemilattice` `Mathlib.CategoryTheory.ChosenFiniteProducts` `Mathlib.CategoryTheory.Closed.Cartesian` `Mathlib.CategoryTheory.Closed.Enrichment` `Mathlib.CategoryTheory.Closed.FunctorCategory.Complete` `Mathlib.CategoryTheory.Closed.FunctorCategory.Groupoid` `Mathlib.CategoryTheory.Closed.FunctorToTypes` `Mathlib.CategoryTheory.Closed.Functor` `Mathlib.CategoryTheory.Closed.Ideal` `Mathlib.CategoryTheory.Closed.Monoidal` `Mathlib.CategoryTheory.Closed.Types` `Mathlib.CategoryTheory.Closed.Zero` `Mathlib.CategoryTheory.Comma.Final` `Mathlib.CategoryTheory.Comma.Presheaf.Colimit` `Mathlib.CategoryTheory.ConcreteCategory.Elementwise` `Mathlib.CategoryTheory.ConcreteCategory.EpiMono` `Mathlib.CategoryTheory.Dialectica.Basic` `Mathlib.CategoryTheory.DifferentialObject` `Mathlib.CategoryTheory.Enriched.Basic` `Mathlib.CategoryTheory.Enriched.FunctorCategory` `Mathlib.CategoryTheory.Enriched.HomCongr` `Mathlib.CategoryTheory.Enriched.Opposite` `Mathlib.CategoryTheory.Enriched.Ordinary.Basic` `Mathlib.CategoryTheory.Filtered.CostructuredArrow` `Mathlib.CategoryTheory.Filtered.Final` `Mathlib.CategoryTheory.Filtered.Flat` `Mathlib.CategoryTheory.Filtered.OfColimitCommutesFiniteLimit` `Mathlib.CategoryTheory.Functor.Derived.RightDerived` `Mathlib.CategoryTheory.Functor.Flat` `Mathlib.CategoryTheory.Functor.FunctorHom` `Mathlib.CategoryTheory.GlueData` `Mathlib.CategoryTheory.GradedObject.Associator` `Mathlib.CategoryTheory.GradedObject.Bifunctor` `Mathlib.CategoryTheory.GradedObject.Braiding` `Mathlib.CategoryTheory.GradedObject.Monoidal` `Mathlib.CategoryTheory.GradedObject.Single` `Mathlib.CategoryTheory.GradedObject.Trifunctor` `Mathlib.CategoryTheory.GradedObject.Unitor` `Mathlib.CategoryTheory.GradedObject` `Mathlib.CategoryTheory.GuitartExact.Basic` `Mathlib.CategoryTheory.GuitartExact.VerticalComposition` `Mathlib.CategoryTheory.LiftingProperties.Limits` `Mathlib.CategoryTheory.Limits.ColimitLimit` `Mathlib.CategoryTheory.Limits.Comma` `Mathlib.CategoryTheory.Limits.ConcreteCategory.Basic` `Mathlib.CategoryTheory.Limits.Constructions.BinaryProducts` `Mathlib.CategoryTheory.Limits.Constructions.EpiMono` `Mathlib.CategoryTheory.Limits.Constructions.Equalizers` `Mathlib.CategoryTheory.Limits.Constructions.Over.Products` `Mathlib.CategoryTheory.Limits.Constructions.ZeroObjects` `Mathlib.CategoryTheory.Limits.Elements` `Mathlib.CategoryTheory.Limits.EpiMono` `Mathlib.CategoryTheory.Limits.FilteredColimitCommutesFiniteLimit` `Mathlib.CategoryTheory.Limits.FilteredColimitCommutesProduct` `Mathlib.CategoryTheory.Limits.Filtered` `Mathlib.CategoryTheory.Limits.Final.ParallelPair` `Mathlib.CategoryTheory.Limits.Final` `Mathlib.CategoryTheory.Limits.FunctorCategory.EpiMono` `Mathlib.CategoryTheory.Limits.FunctorCategory.Filtered` `Mathlib.CategoryTheory.Limits.FunctorToTypes` `Mathlib.CategoryTheory.Limits.IndYoneda` `Mathlib.CategoryTheory.Limits.IsConnected` `Mathlib.CategoryTheory.Limits.MonoCoprod` `Mathlib.CategoryTheory.Limits.Opposites` `Mathlib.CategoryTheory.Limits.Over` `Mathlib.CategoryTheory.Limits.Preserves.FunctorCategory` `Mathlib.CategoryTheory.Limits.Preserves.Opposites` `Mathlib.CategoryTheory.Limits.Preserves.Presheaf` `Mathlib.CategoryTheory.Limits.Preserves.Shapes.AbelianImages` `Mathlib.CategoryTheory.Limits.Preserves.Shapes.Biproducts` `Mathlib.CategoryTheory.Limits.Preserves.Shapes.Images` `Mathlib.CategoryTheory.Limits.Preserves.Shapes.Kernels` `Mathlib.CategoryTheory.Limits.Preserves.Shapes.Pullbacks` `Mathlib.CategoryTheory.Limits.Preserves.Shapes.Square` `Mathlib.CategoryTheory.Limits.Preserves.Shapes.Zero` `Mathlib.CategoryTheory.Limits.Preserves.Ulift` `Mathlib.CategoryTheory.Limits.Preserves.Yoneda` `Mathlib.CategoryTheory.Limits.Presheaf` `Mathlib.CategoryTheory.Limits.Shapes.Biproducts` `Mathlib.CategoryTheory.Limits.Shapes.ConcreteCategory` `Mathlib.CategoryTheory.Limits.Shapes.Countable` `Mathlib.CategoryTheory.Limits.Shapes.Diagonal` `Mathlib.CategoryTheory.Limits.Shapes.FunctorToTypes` `Mathlib.CategoryTheory.Limits.Shapes.Images` `Mathlib.CategoryTheory.Limits.Shapes.KernelPair` `Mathlib.CategoryTheory.Limits.Shapes.Kernels` `Mathlib.CategoryTheory.Limits.Shapes.NormalMono.Basic` `Mathlib.CategoryTheory.Limits.Shapes.NormalMono.Equalizers` `Mathlib.CategoryTheory.Limits.Shapes.Pullback.CommSq` `Mathlib.CategoryTheory.Limits.Shapes.Pullback.Equalizer` `Mathlib.CategoryTheory.Limits.Shapes.Pullback.Square` `Mathlib.CategoryTheory.Limits.Shapes.Reflexive` `Mathlib.CategoryTheory.Limits.Shapes.Types` `Mathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms` `Mathlib.CategoryTheory.Limits.Sifted` `Mathlib.CategoryTheory.Limits.TypesFiltered` `Mathlib.CategoryTheory.Limits.Types` `Mathlib.CategoryTheory.Limits.VanKampen` `Mathlib.CategoryTheory.Limits.Yoneda` `Mathlib.CategoryTheory.Linear.Basic` `Mathlib.CategoryTheory.Localization.Adjunction` `Mathlib.CategoryTheory.Localization.Bifunctor` `Mathlib.CategoryTheory.Localization.Bousfield` `Mathlib.CategoryTheory.Localization.CalculusOfFractions.ComposableArrows` `Mathlib.CategoryTheory.Localization.CalculusOfFractions.Fractions` `Mathlib.CategoryTheory.Localization.CalculusOfFractions` `Mathlib.CategoryTheory.Localization.Composition` `Mathlib.CategoryTheory.Localization.Construction` `Mathlib.CategoryTheory.Localization.DerivabilityStructure.Basic` `Mathlib.CategoryTheory.Localization.DerivabilityStructure.Constructor` `Mathlib.CategoryTheory.Localization.Equivalence` `Mathlib.CategoryTheory.Localization.FiniteProducts` `Mathlib.CategoryTheory.Localization.HasLocalization` `Mathlib.CategoryTheory.Localization.HomEquiv` `Mathlib.CategoryTheory.Localization.LocalizerMorphism` `Mathlib.CategoryTheory.Localization.LocallySmall` `Mathlib.CategoryTheory.Localization.Monoidal` `Mathlib.CategoryTheory.Localization.Opposite` `Mathlib.CategoryTheory.Localization.Pi` `Mathlib.CategoryTheory.Localization.Predicate` `Mathlib.CategoryTheory.Localization.Prod` `Mathlib.CategoryTheory.Localization.Resolution` `Mathlib.CategoryTheory.Localization.SmallHom` `Mathlib.CategoryTheory.Localization.StructuredArrow` `Mathlib.CategoryTheory.Localization.Trifunctor` `Mathlib.CategoryTheory.Monad.Adjunction` `Mathlib.CategoryTheory.Monad.Coequalizer` `Mathlib.CategoryTheory.Monad.Comonadicity` `Mathlib.CategoryTheory.Monad.Equalizer` `Mathlib.CategoryTheory.Monad.EquivMon` `Mathlib.CategoryTheory.Monad.Limits` `Mathlib.CategoryTheory.Monad.Monadicity` `Mathlib.CategoryTheory.Monoidal.Bimod` `Mathlib.CategoryTheory.Monoidal.Bimon_` `Mathlib.CategoryTheory.Monoidal.Braided.Basic` `Mathlib.CategoryTheory.Monoidal.Braided.Opposite` `Mathlib.CategoryTheory.Monoidal.Braided.Reflection` `Mathlib.CategoryTheory.Monoidal.Cartesian.Comon_` `Mathlib.CategoryTheory.Monoidal.Center` `Mathlib.CategoryTheory.Monoidal.CommMon_` `Mathlib.CategoryTheory.Monoidal.Comon_` `Mathlib.CategoryTheory.Monoidal.Conv` `Mathlib.CategoryTheory.Monoidal.Discrete` `Mathlib.CategoryTheory.Monoidal.End` `Mathlib.CategoryTheory.Monoidal.Free.Basic` `Mathlib.CategoryTheory.Monoidal.Free.Coherence` `Mathlib.CategoryTheory.Monoidal.FunctorCategory` `Mathlib.CategoryTheory.Monoidal.Functor` `Mathlib.CategoryTheory.Monoidal.Hopf_` `Mathlib.CategoryTheory.Monoidal.Internal.FunctorCategory` `Mathlib.CategoryTheory.Monoidal.Internal.Limits` `Mathlib.CategoryTheory.Monoidal.Internal.Types` `Mathlib.CategoryTheory.Monoidal.Limits` `Mathlib.CategoryTheory.Monoidal.Mod_` `Mathlib.CategoryTheory.Monoidal.Mon_` `Mathlib.CategoryTheory.Monoidal.NaturalTransformation` `Mathlib.CategoryTheory.Monoidal.OfChosenFiniteProducts.Symmetric` `Mathlib.CategoryTheory.Monoidal.OfHasFiniteProducts` `Mathlib.CategoryTheory.Monoidal.Rigid.Basic` `Mathlib.CategoryTheory.Monoidal.Rigid.Braided` `Mathlib.CategoryTheory.Monoidal.Rigid.FunctorCategory` `Mathlib.CategoryTheory.Monoidal.Rigid.OfEquivalence` `Mathlib.CategoryTheory.Monoidal.Skeleton` `Mathlib.CategoryTheory.Monoidal.Transport` `Mathlib.CategoryTheory.Monoidal.Types.Basic` `Mathlib.CategoryTheory.Monoidal.Types.Coyoneda` `Mathlib.CategoryTheory.Monoidal.Types.Symmetric` `Mathlib.CategoryTheory.MorphismProperty.Basic` `Mathlib.CategoryTheory.MorphismProperty.Comma` `Mathlib.CategoryTheory.MorphismProperty.Composition` `Mathlib.CategoryTheory.MorphismProperty.Concrete` `Mathlib.CategoryTheory.MorphismProperty.Factorization` `Mathlib.CategoryTheory.MorphismProperty.IsInvertedBy` `Mathlib.CategoryTheory.MorphismProperty.IsSmall` `Mathlib.CategoryTheory.MorphismProperty.LiftingProperty` `Mathlib.CategoryTheory.MorphismProperty.Limits` `Mathlib.CategoryTheory.MorphismProperty.OverAdjunction` `Mathlib.CategoryTheory.MorphismProperty.Representable` `Mathlib.CategoryTheory.MorphismProperty.Retract` `Mathlib.CategoryTheory.PathCategory.MorphismProperty` `Mathlib.CategoryTheory.Preadditive.Basic` `Mathlib.CategoryTheory.Preadditive.Injective` `Mathlib.CategoryTheory.Preadditive.OfBiproducts` `Mathlib.CategoryTheory.Preadditive.Projective` `Mathlib.CategoryTheory.Preadditive.SingleObj` `Mathlib.CategoryTheory.Shift.Adjunction` `Mathlib.CategoryTheory.Shift.Basic` `Mathlib.CategoryTheory.Shift.CommShift` `Mathlib.CategoryTheory.Shift.Induced` `Mathlib.CategoryTheory.Shift.Localization` `Mathlib.CategoryTheory.Shift.Predicate` `Mathlib.CategoryTheory.Shift.Quotient` `Mathlib.CategoryTheory.Shift.SingleFunctors` `Mathlib.CategoryTheory.Subobject.Basic` `Mathlib.CategoryTheory.Subobject.Comma` `Mathlib.CategoryTheory.Subobject.FactorThru` `Mathlib.CategoryTheory.Subobject.MonoOver` `Mathlib.CategoryTheory.Subobject.Types` `Mathlib.CategoryTheory.Subobject.WellPowered` `Mathlib.CategoryTheory.Subterminal` `Mathlib.CategoryTheory.Triangulated.Basic` `Mathlib.CategoryTheory.Widesubcategory` `Mathlib.Combinatorics.Digraph.Basic` `Mathlib.Order.Category.BddDistLat` `Mathlib.Order.Category.BddLat` `Mathlib.Order.Category.BddOrd` `Mathlib.Order.Category.DistLat` `Mathlib.Order.Category.HeytAlg` `Mathlib.Order.Category.Lat` `Mathlib.Order.Category.LinOrd` `Mathlib.Order.Category.PartOrd` `Mathlib.Order.Category.Preord` `Mathlib.Order.Category.Semilat` `Mathlib.Order.CompleteBooleanAlgebra` `Mathlib.Tactic.CategoryTheory.Coherence`	3
8 files `Mathlib.Algebra.Category.GrpWithZero` `Mathlib.Algebra.Module.LinearMap.Star` `Mathlib.Algebra.Star.Basic` `Mathlib.Algebra.Star.Pi` `Mathlib.Algebra.Star.Prod` `Mathlib.Algebra.Star.StarRingHom` `Mathlib.Data.Fin.Tuple.Curry` `Mathlib.Logic.Equiv.Fin`	7
50 files `Mathlib.Algebra.Algebra.Defs` `Mathlib.Algebra.Category.Grp.Basic` `Mathlib.Algebra.Category.Grp.EquivalenceGroupAddGroup` `Mathlib.Algebra.Category.Grp.FiniteGrp` `Mathlib.Algebra.Category.Grp.ForgetCorepresentable` `Mathlib.Algebra.Category.MonCat.Adjunctions` `Mathlib.Algebra.Category.MonCat.Basic` `Mathlib.Algebra.Category.MonCat.ForgetCorepresentable` `Mathlib.Algebra.Category.Ring.Basic` `Mathlib.Algebra.Group.Action.Basic` `Mathlib.Algebra.Group.Action.Pi` `Mathlib.Algebra.Group.Aut` `Mathlib.Algebra.Group.Conj` `Mathlib.Algebra.Group.Submonoid.DistribMulAction` `Mathlib.Algebra.Group.Submonoid.MulAction` `Mathlib.Algebra.GroupWithZero.Action.Basic` `Mathlib.Algebra.GroupWithZero.Action.Pi` `Mathlib.Algebra.GroupWithZero.Conj` `Mathlib.Algebra.Module.Equiv.Basic` `Mathlib.Algebra.Module.Equiv.Defs` `Mathlib.Algebra.Module.Equiv.Opposite` `Mathlib.Algebra.Module.Hom` `Mathlib.Algebra.Module.LinearMap.Basic` `Mathlib.Algebra.Module.LinearMap.Defs` `Mathlib.Algebra.Module.LinearMap.End` `Mathlib.Algebra.Module.LinearMap.Prod` `Mathlib.Algebra.Module.Pi` `Mathlib.Algebra.Module.ULift` `Mathlib.Algebra.NoZeroSMulDivisors.Pi` `Mathlib.Algebra.Ring.Action.Group` `Mathlib.Algebra.Ring.Action.Invariant` `Mathlib.Algebra.Ring.Action.Subobjects` `Mathlib.Algebra.Ring.AddAut` `Mathlib.Algebra.Ring.Aut` `Mathlib.Algebra.Ring.Fin` `Mathlib.CategoryTheory.Sites.NonabelianCohomology.H1` `Mathlib.Data.List.Sublists` `Mathlib.Data.Matrix.Defs` `Mathlib.Data.Matrix.Diagonal` `Mathlib.Dynamics.FixedPoints.Basic` `Mathlib.GroupTheory.GroupAction.DomAct.ActionHom` `Mathlib.GroupTheory.GroupAction.DomAct.Basic` `Mathlib.GroupTheory.GroupAction.Embedding` `Mathlib.GroupTheory.OreLocalization.Basic` `Mathlib.GroupTheory.Perm.Basic` `Mathlib.GroupTheory.Perm.ViaEmbedding` `Mathlib.LinearAlgebra.GeneralLinearGroup` `Mathlib.Order.Interval.Set.WithBotTop` `Mathlib.Order.RelIso.Set` `Mathlib.RingTheory.OreLocalization.Basic`	8
30 files `Mathlib.Algebra.Group.Fin.Basic` `Mathlib.Algebra.Group.Fin.Tuple` `Mathlib.Algebra.Module.End` `Mathlib.Algebra.Module.NatInt` `Mathlib.Algebra.NoZeroSMulDivisors.Basic` `Mathlib.Algebra.Order.GroupWithZero.Bounds` `Mathlib.Algebra.Order.Kleene` `Mathlib.Algebra.Order.Pi` `Mathlib.Algebra.Order.Ring.Prod` `Mathlib.Data.Array.Lemmas` `Mathlib.Data.Fin.Basic` `Mathlib.Data.Fin.Rev` `Mathlib.Data.Fin.Tuple.Basic` `Mathlib.Data.Fin.Tuple.Take` `Mathlib.Data.Fin.VecNotation` `Mathlib.Data.List.ChainOfFn` `Mathlib.Data.List.FinRange` `Mathlib.Data.List.OfFn` `Mathlib.Data.Nat.Prime.Infinite` `Mathlib.Data.Num.Bitwise` `Mathlib.Data.Vector.Basic` `Mathlib.Data.Vector.MapLemmas` `Mathlib.Data.Vector.Mem` `Mathlib.Data.Vector.Snoc` `Mathlib.Data.Vector.Zip` `Mathlib.Logic.Embedding.Set` `Mathlib.Logic.Equiv.Embedding` `Mathlib.Logic.Function.FromTypes` `Mathlib.Logic.Function.OfArity` `Mathlib.Logic.Small.List`	9
10 files `Mathlib.Algebra.BigOperators.Group.List.Lemmas` `Mathlib.Algebra.Field.ULift` `Mathlib.Algebra.Ring.CompTypeclasses` `Mathlib.Algebra.Ring.Equiv` `Mathlib.Algebra.Ring.Pi` `Mathlib.Algebra.Ring.Prod` `Mathlib.Algebra.Ring.ULift` `Mathlib.Data.List.Permutation` `Mathlib.Data.List.Prime` `Mathlib.RingTheory.RingInvo`	10
43 files `Mathlib.Algebra.Group.Pi.Lemmas` `Mathlib.Algebra.Order.Group.Bounds` `Mathlib.Algebra.Order.Group.PiLex` `Mathlib.Algebra.Order.Interval.Set.Monoid` `Mathlib.CategoryTheory.Category.ReflQuiv` `Mathlib.Combinatorics.Quiver.Arborescence` `Mathlib.Combinatorics.Quiver.ReflQuiver` `Mathlib.Data.Bool.Set` `Mathlib.Data.Countable.Small` `Mathlib.Data.List.AList` `Mathlib.Data.List.Dedup` `Mathlib.Data.List.Duplicate` `Mathlib.Data.List.Lemmas` `Mathlib.Data.List.NatAntidiagonal` `Mathlib.Data.List.Nodup` `Mathlib.Data.List.Perm.Lattice` `Mathlib.Data.List.Rotate` `Mathlib.Data.List.Sigma` `Mathlib.Data.Nat.Set` `Mathlib.Data.Prod.TProd` `Mathlib.Data.Set.Function` `Mathlib.Data.Set.Image` `Mathlib.Data.Set.List` `Mathlib.Data.Set.Monotone` `Mathlib.Data.Set.NAry` `Mathlib.Data.Set.Pairwise.Basic` `Mathlib.Data.Set.Prod` `Mathlib.Logic.Equiv.PartialEquiv` `Mathlib.Logic.Equiv.Set` `Mathlib.Logic.Small.Basic` `Mathlib.Order.Bounds.Basic` `Mathlib.Order.Bounds.Image` `Mathlib.Order.ConditionallyCompleteLattice.Defs` `Mathlib.Order.Directed` `Mathlib.Order.Interval.Set.Image` `Mathlib.Order.Interval.Set.SurjOn` `Mathlib.Order.Interval.Set.UnorderedInterval` `Mathlib.Order.LatticeIntervals` `Mathlib.Order.Monotone.Odd` `Mathlib.Order.Monotone.Union` `Mathlib.Order.PiLex` `Mathlib.Order.ScottContinuity` `Mathlib.Order.WellFounded`	11
`Mathlib.Algebra.Group.Subgroup.Even` `Mathlib.Algebra.Ring.Subring.Defs`	12
5 files `Mathlib.Algebra.Field.Opposite` `Mathlib.Algebra.Ring.Center` `Mathlib.Data.Int.Cast.Lemmas` `Mathlib.Tactic.NormNum.PowMod` `Mathlib.Tactic.NormNum.Pow`	13
3 files `Mathlib.Data.Set.SymmDiff` `Mathlib.Order.SymmDiff` `Mathlib.Tactic.TautoSet`	14
3 files `Mathlib.Algebra.GroupWithZero.Submonoid` `Mathlib.Algebra.PUnitInstances.Order` `Mathlib.RingTheory.NonUnitalSubring.Defs`	23
`Mathlib.Algebra.Ring.Hom.Basic`	24
`Mathlib.Algebra.Group.Subgroup.Defs`	25
`Mathlib.Data.Set.Enumerate`	27
6 files `Mathlib.Algebra.Order.GroupWithZero.Submonoid` `Mathlib.Algebra.Order.Interval.Set.Instances` `Mathlib.Algebra.Ring.Subsemiring.Defs` `Mathlib.GroupTheory.Subsemigroup.Center` `Mathlib.Order.Heyting.Boundary` `Mathlib.RingTheory.NonUnitalSubsemiring.Defs`	28
4 files `Mathlib.Algebra.Group.Center` `Mathlib.Algebra.GroupWithZero.Center` `Mathlib.Algebra.Ring.Centralizer` `Mathlib.Data.PEquiv`	29
4 files `Mathlib.Algebra.Group.Submonoid.Defs` `Mathlib.Algebra.Group.Subsemigroup.Defs` `Mathlib.GroupTheory.OreLocalization.OreSet` `Mathlib.RingTheory.OreLocalization.OreSet`	30
`Mathlib.Data.SetLike.Basic`	31
11 files `Mathlib.Data.Bundle` `Mathlib.Data.Nat.Order.Lemmas` `Mathlib.Data.Part` `Mathlib.Data.Set.Basic` `Mathlib.Data.Set.BoolIndicator` `Mathlib.Data.Set.Subsingleton` `Mathlib.Logic.Function.FiberPartition` `Mathlib.Order.Bounded` `Mathlib.Order.Circular` `Mathlib.Order.Filter.Defs` `Mathlib.Order.Interval.Set.Basic`	32
`Mathlib.Order.BooleanAlgebra` `Mathlib.Order.Heyting.Basic`	36

Declarations diff

+ gc_inf_himp
+ gc_sdiff_sup
-+-+-+ of

You can run this locally as follows

## summary with just the declaration names:
./scripts/declarations_diff.sh <optional_commit>

## more verbose report:
./scripts/declarations_diff.sh long <optional_commit>

The doc-module for script/declarations_diff.sh contains some details about this script.

No changes to technical debt.

You can run this locally as

./scripts/technical-debt-metrics.sh pr_summary

The relative value is the weighted sum of the differences with weight given by the inverse of the current value of the statistic.
The absolute value is the relative value divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).

YaelDillies

Nice find! Can you do the same thing for coframe?

Bergschaf · 2025-02-04T12:21:27Z

It seems like the documentation for (Generalized) Coheyting Algebras is wrong, because it claims that "A generalized co-Heyting algebra is a lattice with an additional binary difference operation \ such that (· \ a) is right adjoint to (· ⊔ a)."
But the supremum is actually the right adjoint, right? (Because it preserves infima)

YaelDillies · 2025-02-04T12:30:22Z

Very possible! I always get the directions wrong

Bergschaf · 2025-02-04T12:48:29Z

Very possible! I always get the directions wrong

I created a PR here: #21418

Mathlib/Order/CompleteBooleanAlgebra.lean

Mathlib/Data/Fintype/Order.lean

Mathlib/Order/CompleteBooleanAlgebra.lean

YaelDillies

Thanks! 🚀

maintainer merge

github-actions · 2025-02-04T19:59:28Z

🚀 Pull request has been placed on the maintainer queue by YaelDillies.

jcommelin

Thanks 🎉

bors merge

… 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).

mathlib-bors · 2025-02-05T06:12:52Z

Pull request successfully merged into master.

Build succeeded:

* origin/master: (103 commits) chore(PresheafedSpace): remove `mk_coe` and some comments from porting (#21382) refactor(CategoryTheory): `ConcreteCategory` instance for `FintypeCat` (#21466) refactor(Algebra/Category): clean up remaining uses of `HasForget` (#21460) chore(Algebra/Field/Basic): make some arguments implicit (#21453) chore(LinearAlgebra/TensorProduct): upgrade `TensorProduct.prodRight` (#21432) docs(Logic/Function/Defs): missing backticks (#21459) style(Logic/Embedding/Set): unindent (#21457) doc: document design choice of (AE)StronglyMeasurable.enorm and `edist` (#21423) perf(RingTheory/Artinian): reorder arguments in `IsArtinianRing.isMaximal_of_isPrime` (#21449) feat(Probability): first two derivatives of `cgf` (#21223) feat(RingTheory): `Ring.KrullDimLE` type class (#21452) chore(Probability/ProbabilityMassFunction/Binomial): typo "bernoulli" (#21455) chore: remove unused argument (#21393) feat(MeasureTheory/Integral/RieszMarkovKakutani) prove that the Riesz content is regular and define the Riesz measure (#20040) chore(Topology/Algebra/ContinuousMonoidHom): do not depend on `ContinuousLinearMap` (#21443) doc(CategoryTheory/Monoidal/Category): fix expression in docs (#21445) refactor(Order/CompleteBooleanAlgebra): a complete lattice which is a Heyting algebra is automatically a frame (#21391) chore: cleanup porting notes in TuringMachine (#20821) chore: remove @[simp] when the discr_key is a lambda (#21395) feat/doc: split files, add documentation (#21421) feat(Data/Set/Lattice): iUnion + insertion (#21322) feat(Factorial): k! divides the product of any k successive integers (#21332) feat(CI): bench-after-CI (#21414) feat: primitive group actions (#12052) feat(Algebra/GroupWithZero/Int): add lemmas about Zm0 (#21370) feat(CategoryTheory): small classes of morphisms (#21411) feat(CategoryTheory): (co)limits of constant functors (#21412) chore: rename isUnit_ofPowEqOne (#21407) chore: split mapDomain out of MonoidAlgebra.Defs (#21398) chore: generalise lemmas to `ENorm` spaces, part 1 (#21380) chore: add `simp` to `Setoid.refl` (#21107) chore: tidy various files (#21406) chore(Geometry/Manifold/IsManifold): split out material on extended charts (#21219) refactor: introduce `Ideal.IsTwoSided` class for quotients of noncommutative rings (#17930) chore(Algebra/Category/ModuleCat): delete `ModuleCat.hasForgetModuleCat` (#21425) feat(RingTheory): unramified iff `κ(q)/κ(p)` is separable and `pS_q = qS_q` (#20690) doc(Order/Heyting/Basic): Coheyting difference is not right adjoint but left adjoint (#21418) chore: move ProofWidgets to v0.0.51 (#21416) chore: rename mem_nonZeroDivisor_of_injective and comap_nonZeroDivisor_le_of_injective (#21408) feat: drop ordering assumption in `RootPairing.coxeterWeight_mem_set_of_isCrystallographic` (#21122) feat(AlgebraicGeometry): the diagonal of an unramified morphism is an open immersion (#21386) feat(Data/LinearIndependent): iff versions of smul action on independent sets (#21383) chore(Combinatorics/SimpleGraph): Fix `hadj` naming (#21389) chore: rename AnalyticAt.order_neq_top_iff (#21388) fix: bug in daily.yml (#21401) chore: remove `@[simp]` from `CategoryTheory.Discrete.functor_map` (#21392) chore(Algebra/PUnitInstances): generalise universes (#21381) feat(RingTheory/PowerSeries): describe when power series map is zero (#21379) feat(Tactic/Linter): options to in/exclude definitions and private decls (#21374) feat: the prime spectrum is quasi-separated (#21362) ...

… 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).

Bergschaf added 3 commits February 3, 2025 21:48

commit

8dc01a0

commit

365f359

whitespace

c178432

Bergschaf added the RFC Request for comment label Feb 3, 2025

Bergschaf requested a review from YaelDillies February 3, 2025 20:57

github-actions bot added the t-order Order theory label Feb 3, 2025

Bergschaf removed the request for review from YaelDillies February 3, 2025 21:35

Bergschaf added 2 commits February 4, 2025 12:33

builds?

365742b

builds?

4a6023e

Bergschaf requested a review from YaelDillies February 4, 2025 11:54

YaelDillies reviewed Feb 4, 2025

View reviewed changes

YaelDillies added the awaiting-author A reviewer has asked the author a question or requested changes. label Feb 4, 2025

Bergschaf added 2 commits February 4, 2025 13:33

coframe

bf9dc53

fix

69390a0

YaelDillies mentioned this pull request Feb 4, 2025

[Merged by Bors] - doc(Order/Heyting/Basic): Coheyting difference is not right adjoint but left adjoint #21418

Closed

Bergschaf removed awaiting-author A reviewer has asked the author a question or requested changes. RFC Request for comment labels Feb 4, 2025

Bergschaf requested a review from YaelDillies February 4, 2025 14:03

YaelDillies reviewed Feb 4, 2025

View reviewed changes

YaelDillies added the awaiting-author A reviewer has asked the author a question or requested changes. label Feb 4, 2025

Bergschaf added 3 commits February 4, 2025 15:38

galoisConnection

6b665e9

protected

6700f99

s

bdb24d2

github-actions bot added the large-import Automatically added label for PRs with a significant increase in transitive imports label Feb 4, 2025

eq

1767896

YaelDillies reviewed Feb 4, 2025

View reviewed changes

Mathlib/Order/CompleteBooleanAlgebra.lean Outdated Show resolved Hide resolved

Bergschaf added 2 commits February 4, 2025 16:06

remove le version

2b0081d

fix

070db3a

Bergschaf removed the awaiting-author A reviewer has asked the author a question or requested changes. label Feb 4, 2025

Bergschaf requested a review from YaelDillies February 4, 2025 18:57

YaelDillies reviewed Feb 4, 2025

View reviewed changes

YaelDillies added the awaiting-author A reviewer has asked the author a question or requested changes. label Feb 4, 2025

Bergschaf added 2 commits February 4, 2025 20:50

remove root

7871269

remove root

c28f3b5

Bergschaf added awaiting-author A reviewer has asked the author a question or requested changes. and removed awaiting-author A reviewer has asked the author a question or requested changes. labels Feb 4, 2025

Bergschaf added 2 commits February 4, 2025 20:54

oops

b826d7d

oops2

42e09d9

Bergschaf removed the awaiting-author A reviewer has asked the author a question or requested changes. label Feb 4, 2025

YaelDillies approved these changes Feb 4, 2025

View reviewed changes

github-actions bot added the maintainer-merge A reviewer has approved the changed; awaiting maintainer approval. label Feb 4, 2025

YaelDillies changed the title ~~feat(Order/CompleteBooleanAlgebra): It suffices for a Frame to be a Complete Lattice and a Heyting Algebra~~ refactor(Order/CompleteBooleanAlgebra): a complete lattice which is a Heyting algebra is automatically a frame Feb 4, 2025

jcommelin reviewed Feb 5, 2025

View reviewed changes

ghost added ready-to-merge This PR has been sent to bors. and removed maintainer-merge A reviewer has approved the changed; awaiting maintainer approval. labels Feb 5, 2025

mathlib-bors bot changed the title ~~refactor(Order/CompleteBooleanAlgebra): a complete lattice which is a Heyting algebra is automatically a frame~~ [Merged by Bors] - refactor(Order/CompleteBooleanAlgebra): a complete lattice which is a Heyting algebra is automatically a frame Feb 5, 2025

mathlib-bors bot closed this Feb 5, 2025

mathlib-bors bot deleted the CompleteHeytingAlgebra branch February 5, 2025 06:12

Conversation

Bergschaf commented Feb 3, 2025 • edited by YaelDillies Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

github-actions bot commented Feb 3, 2025 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

PR summary 42e09d9688

Import changes for modified files

Declarations diff

Uh oh!

YaelDillies left a comment

Choose a reason for hiding this comment

Uh oh!

Bergschaf commented Feb 4, 2025

Uh oh!

YaelDillies commented Feb 4, 2025

Uh oh!

Bergschaf commented Feb 4, 2025

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

YaelDillies left a comment

Choose a reason for hiding this comment

Uh oh!

github-actions bot commented Feb 4, 2025

Uh oh!

jcommelin left a comment

Choose a reason for hiding this comment

Uh oh!

mathlib-bors bot commented Feb 5, 2025

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

3 participants

Bergschaf commented Feb 3, 2025 •

edited by YaelDillies

Loading

github-actions bot commented Feb 3, 2025 •

edited

Loading