Mathlib v3 is deprecated. Go to Mathlib v4

Theorem initial_seg.init

Modification history

2023-03-02 13:10

src/order/initial_seg.lean

chore(set_theory/ordinal/initial_seg): swap the names of `init` and `init'` (#18534) …

Added initial_seg.init View on Github →