Mathlib v3 is deprecated. Go to Mathlib v4

Def ordinal.initial_seg_out

Modification history

2022-03-07 10:15

src/set_theory/ordinal.lean

refactor(set_theory/*): `o.out.r` → `<` (#12468) …

Modified ordinal.initial_seg_out View on Github →

2019-05-10 00:53

src/set_theory/ordinal.lean

feat(set_theory): add to cardinal, ordinal, cofinality (#963) …

Added ordinal.initial_seg_out View on Github →