Commit 2024-10-10 11:25 989faa24

View on Github →

feat(Order/InitSeg): notation for initial and principal segments of < (#17481) We introduce the notations α ≤i β and α <i β for initial/principal segment embeddings between the < relations of two types. We also prove a few lemmas.

Estimated changes

Modified Mathlib/Order/InitialSeg.lean

added theorem InitialSeg.coe_toOrderEmbedding

added theorem InitialSeg.le_apply_iff

added theorem InitialSeg.le_iff_le

added theorem InitialSeg.lt_apply_iff

added theorem InitialSeg.lt_iff_lt

added theorem InitialSeg.mem_range_of_le

added theorem InitialSeg.monotone

added theorem InitialSeg.strictMono

added def InitialSeg.toOrderEmbedding

added theorem InitialSeg.toOrderEmbedding_apply

added theorem PrincipalSeg.le_apply_iff

added theorem PrincipalSeg.le_iff_le

added theorem PrincipalSeg.lt_apply_iff

added theorem PrincipalSeg.lt_iff_lt

added theorem PrincipalSeg.mem_range_of_le

added theorem PrincipalSeg.monotone

added theorem PrincipalSeg.strictMono

Modified Mathlib/SetTheory/Ordinal/Basic.lean

modified def Ordinal.initialSegToType

modified def Ordinal.liftInitialSeg

modified def Ordinal.liftPrincipalSeg

modified def Ordinal.principalSegToType