Mathlib v3 is deprecated. Go to Mathlib v4

Def well_ordering_rel

Modification history

2019-07-01 17:57
src/set_theory/ordinal.lean
refactor(set_theory/ordinal): restate well_ordering_thm (#1115) …
Added well_ordering_relView on Github →