Mathlib v3 is deprecated. Go to Mathlib v4

Theorem principal_seg.apply_subrel_iso

Modification history

2023-07-19 06:33
src/order/initial_seg.lean
chore(set_theory/ordinal/basic): golf (#18547)
Added principal_seg.apply_subrel_isoView on Github →