Commit 2024-10-18 10:35 1cc3f60d

View on Github →

chore(Order/RelIso/Set): golf wellFounded_iff_wellFounded_subrel (#17606) We also move it out of the initial segment file - it doesn't need that machinery to be proven.

Estimated changes

Modified Mathlib/Order/InitialSeg.lean

deleted theorem wellFounded_iff_wellFounded_subrel

Modified Mathlib/Order/RelIso/Set.lean

added theorem Acc.of_subrel

added theorem wellFounded_iff_wellFounded_subrel