Commit 2025-03-13 11:07 6dcd19f5

View on Github →

chore: review of porting notes in Order/ (#22895)

Estimated changes

Modified Mathlib/Order/Antisymmetrization.lean

modified theorem toAntisymmetrization_mono

Modified Mathlib/Order/Basic.lean

Modified Mathlib/Order/BooleanAlgebra.lean

Modified Mathlib/Order/BoundedOrder/Basic.lean

Modified Mathlib/Order/Bounds/OrderIso.lean

Modified Mathlib/Order/Circular.lean

Modified Mathlib/Order/Compare.lean

Modified Mathlib/Order/CompleteLattice.lean

Modified Mathlib/Order/ConditionallyCompleteLattice/Basic.lean

Modified Mathlib/Order/ConditionallyCompleteLattice/Defs.lean

Modified Mathlib/Order/Directed.lean

Modified Mathlib/Order/Disjoint.lean

modified theorem Complementeds.coe_lt_coe

modified theorem Complementeds.mk_bot

modified theorem Complementeds.mk_top

Modified Mathlib/Order/Filter/AtTopBot/Basic.lean

Modified Mathlib/Order/Filter/AtTopBot/Finite.lean

Modified Mathlib/Order/Filter/AtTopBot/Finset.lean

Modified Mathlib/Order/Filter/Bases/Basic.lean

Modified Mathlib/Order/Filter/Basic.lean

Modified Mathlib/Order/Filter/CountablyGenerated.lean

Modified Mathlib/Order/Filter/Finite.lean

Modified Mathlib/Order/Filter/Germ/Basic.lean

Modified Mathlib/Order/Filter/Lift.lean

Modified Mathlib/Order/FixedPoints.lean

Modified Mathlib/Order/GaloisConnection/Defs.lean

Modified Mathlib/Order/Height.lean

Modified Mathlib/Order/Heyting/Boundary.lean

Modified Mathlib/Order/Heyting/Regular.lean

Modified Mathlib/Order/Hom/Basic.lean

Modified Mathlib/Order/Hom/Bounded.lean

Modified Mathlib/Order/Hom/CompleteLattice.lean

Modified Mathlib/Order/Hom/Lattice.lean

Modified Mathlib/Order/Hom/Order.lean

Modified Mathlib/Order/Ideal.lean

Modified Mathlib/Order/InitialSeg.lean

Modified Mathlib/Order/Interval/Basic.lean

Modified Mathlib/Order/Interval/Set/Basic.lean

Modified Mathlib/Order/Interval/Set/IsoIoo.lean

Modified Mathlib/Order/Interval/Set/OrdConnected.lean

Modified Mathlib/Order/Interval/Set/UnorderedInterval.lean

Modified Mathlib/Order/JordanHolder.lean

Modified Mathlib/Order/LiminfLimsup.lean

Modified Mathlib/Order/Max.lean

Modified Mathlib/Order/MinMax.lean

Modified Mathlib/Order/Monotone/Basic.lean

Modified Mathlib/Order/Monotone/Defs.lean

Modified Mathlib/Order/OmegaCompletePartialOrder.lean

Modified Mathlib/Order/OrdContinuous.lean

Modified Mathlib/Order/Partition/Finpartition.lean

Modified Mathlib/Order/SetNotation.lean

Modified Mathlib/Order/Synonym.lean

modified theorem OrderDual.ofDual_inj

modified theorem OrderDual.toDual_inj

modified theorem ofLex_inj

modified theorem toLex_inj

Modified Mathlib/Order/TypeTags.lean

Modified Mathlib/Order/UpperLower/Basic.lean

Modified Mathlib/Order/UpperLower/Hom.lean

Modified Mathlib/Order/WellFounded.lean

Modified Mathlib/Order/WellFoundedSet.lean

Modified Mathlib/Order/WithBot.lean

Modified Mathlib/Order/Zorn.lean