Commit 2024-11-04 23:02 5dc964a0

View on Github →

chore(*): LinearOrder + IsWellOrder α (· < ·) → LinearOrder + WellFoundedLT (#18217) These hypotheses are equivalent, but the former spelling contains duplicated hypotheses throughout both typeclasses.

Estimated changes

Modified Mathlib/Algebra/Order/Group/PiLex.lean

Modified Mathlib/Analysis/InnerProductSpace/GramSchmidtOrtho.lean

Modified Mathlib/Data/ENat/Basic.lean

Modified Mathlib/Data/Finsupp/PWO.lean

modified theorem Finsupp.isPWO

Modified Mathlib/Data/Fintype/Card.lean

Modified Mathlib/Data/Nat/PartENat.lean

Modified Mathlib/Data/PNat/Basic.lean

Modified Mathlib/LinearAlgebra/Matrix/LDL.lean

Modified Mathlib/Order/Monotone/Basic.lean

Modified Mathlib/Order/PiLex.lean

Modified Mathlib/Order/RelClasses.lean

Modified Mathlib/Probability/Process/HittingTime.lean

modified theorem MeasureTheory.hitting_isStoppingTime

modified theorem MeasureTheory.hitting_le_iff_of_exists

modified theorem MeasureTheory.hitting_le_iff_of_lt

modified theorem MeasureTheory.hitting_lt_iff

modified theorem MeasureTheory.hitting_mem_set

modified theorem MeasureTheory.hitting_mem_set_of_hitting_lt

modified theorem MeasureTheory.stoppedValue_hitting_mem

Modified Mathlib/SetTheory/Cardinal/Basic.lean

Modified Mathlib/SetTheory/Ordinal/Basic.lean

modified theorem List.Sorted.lt_ord_of_lt

Modified Mathlib/SetTheory/Ordinal/NaturalOps.lean

Modified Mathlib/SetTheory/Ordinal/Nimber.lean

Modified Mathlib/SetTheory/Ordinal/Notation.lean

Modified Mathlib/Topology/Category/Profinite/Nobeling.lean

modified theorem Profinite.NobelingProof.GoodProducts.span

modified theorem Profinite.NobelingProof.GoodProducts.spanFin

modified theorem Profinite.NobelingProof.GoodProducts.span_iff_products