Theorem PrincipalSeg.subrelIso_apply

Modification history

2024-10-08 07:22

Mathlib/Order/InitialSeg.lean

chore(Order/InitialSeg): `PrincipalSeg.down` → `PrincipalSeg.mem_range_iff_rel` (#17516) …

Modified PrincipalSeg.subrelIso_apply View on Github →

2023-07-20 00:27

Mathlib/Order/InitialSeg.lean

chore: golf `set_theory/ordinal/basic` (#5581)

Added PrincipalSeg.subrelIso_apply View on Github →