Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-03-07 10:15 d704f27e

View on Github →

refactor(set_theory/*): o.out.r → < (#12468) We declare a linear_order instance on o.out.α, for o : ordinal, with < def-eq to o.out.r. This will improve code clarity and will allow us to state theorems about specific ordinals as ordered structures.

Estimated changes

added def ordinal.out'
deleted def ordinal.out
deleted theorem ordinal.type_out'
modified theorem pgame.nim.nim_wf_lemma
modified theorem cardinal.card_typein_out_lt
modified def ordinal.rel_iso_out
modified theorem ordinal.type_lt
added theorem ordinal.type_lt_iff
deleted theorem ordinal.type_out
modified theorem ordinal.typein_lt_self
modified theorem ordinal.lsub_typein
modified theorem ordinal.sup_typein_succ