Commit 2026-03-12 15:45 79471657

View on Github →

chore: use IsLUB IsGLB in CompleteLattice (#35328)

Estimated changes

Modified Mathlib/Algebra/Group/Submonoid/Saturation.lean

Modified Mathlib/Algebra/Module/Submodule/Lattice.lean

Modified Mathlib/AlgebraicGeometry/IdealSheaf/Basic.lean

Modified Mathlib/AlgebraicTopology/SimplicialComplex/Basic.lean

Modified Mathlib/CategoryTheory/Sites/Sieves.lean

Modified Mathlib/CategoryTheory/Subfunctor/Basic.lean

Modified Mathlib/CategoryTheory/Subobject/Lattice.lean

Modified Mathlib/Combinatorics/Digraph/Basic.lean

Modified Mathlib/Combinatorics/SimpleGraph/Basic.lean

Modified Mathlib/Combinatorics/SimpleGraph/Subgraph.lean

Modified Mathlib/Data/Fintype/Order.lean

Modified Mathlib/Data/Set/BooleanAlgebra.lean

Modified Mathlib/Geometry/Convex/Cone/Basic.lean

Modified Mathlib/LinearAlgebra/AffineSpace/AffineSubspace/Defs.lean

Modified Mathlib/MeasureTheory/Measure/MeasureSpace.lean

Modified Mathlib/Order/Atoms.lean

Modified Mathlib/Order/Bounds/Image.lean

modified theorem isLUB_prod

Modified Mathlib/Order/CompactlyGenerated/Basic.lean

Modified Mathlib/Order/CompleteBooleanAlgebra.lean

Modified Mathlib/Order/CompleteLattice/Basic.lean

added theorem sInf_apply_eq_sInf_image

added theorem sSup_apply_eq_sSup_image

Modified Mathlib/Order/CompleteLattice/Defs.lean

modified theorem le_sSup

modified theorem sSup_le

Modified Mathlib/Order/CompleteLattice/Lemmas.lean

Modified Mathlib/Order/CompleteLattice/PiLex.lean

Modified Mathlib/Order/CompleteLatticeIntervals.lean

Modified Mathlib/Order/Concept.lean

Modified Mathlib/Order/ConditionallyCompleteLattice/Basic.lean

Modified Mathlib/Order/Copy.lean

Modified Mathlib/Order/Filter/Basic.lean

Modified Mathlib/Order/FixedPoints.lean

Modified Mathlib/Order/GaloisConnection/Basic.lean

Modified Mathlib/Order/Hom/Order.lean

Modified Mathlib/Order/Interval/Basic.lean

Modified Mathlib/Order/Nucleus.lean

Modified Mathlib/Order/ScottContinuity/Prod.lean

Modified Mathlib/Order/SupClosed.lean

Modified Mathlib/Probability/Process/Filtration.lean

Modified Mathlib/RingTheory/TwoSidedIdeal/Lattice.lean

Modified Mathlib/Topology/Algebra/Group/GroupTopology.lean

Modified Mathlib/Topology/Algebra/Module/ClosedSubmodule.lean

Modified Mathlib/Topology/Algebra/Ring/Basic.lean

Modified Mathlib/Topology/UniformSpace/Basic.lean