Commit 2025-08-28 17:49 fc8660bf

View on Github →

chore(Order): review porting notes (#29073) Go through all the porting notes and fix the ones that are easy to apply.

Estimated changes

Modified Mathlib/Order/Category/OmegaCompletePartialOrder.lean

Modified Mathlib/Order/CompleteLattice/Lemmas.lean

Modified Mathlib/Order/CountableDenseLinearOrder.lean

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

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

Modified Mathlib/Order/Filter/Pointwise.lean

Modified Mathlib/Order/FixedPoints.lean

Modified Mathlib/Order/Monotone/Basic.lean

modified theorem antitoneOn_toDual_comp_iff

modified theorem antitone_toDual_comp_iff

modified theorem monotoneOn_toDual_comp_iff

modified theorem monotone_toDual_comp_iff

Modified Mathlib/Order/OmegaCompletePartialOrder.lean

added theorem OmegaCompletePartialOrder.Chain.ext