Mathlib v3 is deprecated. Go to Mathlib v4

Theorem function.well_founded.self_le_of_strict_mono

Modification history

2022-02-11 01:36
src/order/well_founded.lean
refactor(order/well_founded, set_theory/ordinal_arithmetic): Fix namespace in `self_le_of_strict_mono` (#11871) …
Deleted function.well_founded.self_le_of_strict_monoView on Github →
2021-12-13 19:31
src/order/well_founded.lean
feat(order/well_founded) Added `strict_mono.id_le_of_wo` (#10732) …
Added function.well_founded.self_le_of_strict_monoView on Github →