Mathlib v3 is deprecated. Go to Mathlib v4

Theorem well_founded.eq_strict_mono_iff_eq_range

Modification history

2022-02-14 10:22
src/order/well_founded.lean
feat(order/well_founded, set_theory/ordinal_arithmetic): `eq_strict_mono_iff_eq_range` (#11882) …
Added well_founded.eq_strict_mono_iff_eq_rangeView on Github →