Commit 2022-12-14 23:20 922a88c4

View on Github →

feat port: Order.InitialSeg (#1012) ee0c179cd3c8a45aa5bffbf1b41d8dbede452865

Estimated changes

Modified Mathlib.lean

Created Mathlib/Order/InitialSeg.lean

added theorem InitialSeg.Antisymm.aux

added def InitialSeg.antisymm

added theorem InitialSeg.antisymm_symm

added theorem InitialSeg.antisymm_to_fun

added def InitialSeg.codRestrict

added theorem InitialSeg.cod_restrict_apply

added theorem InitialSeg.coe_coe_fn

added theorem InitialSeg.eq_or_principal

added theorem InitialSeg.init'

added theorem InitialSeg.init_iff

added def InitialSeg.leAdd

added theorem InitialSeg.leAdd_apply

added theorem InitialSeg.le_lt_apply

added theorem InitialSeg.lt_or_eq_apply_left

added theorem InitialSeg.lt_or_eq_apply_right

added def InitialSeg.ofIsEmpty

added def InitialSeg.ofIso

added theorem InitialSeg.refl_apply

added theorem InitialSeg.trans_apply

added theorem InitialSeg.unique_of_trichotomous_of_irrefl

added structure InitialSeg

added def PrincipalSeg.codRestrict

added theorem PrincipalSeg.cod_restrict_apply

added theorem PrincipalSeg.cod_restrict_top

added theorem PrincipalSeg.coe_coe_fn'

added theorem PrincipalSeg.coe_fn_mk

added theorem PrincipalSeg.down

added def PrincipalSeg.equivLt

added theorem PrincipalSeg.equiv_lt_apply

added theorem PrincipalSeg.equiv_lt_top

added theorem PrincipalSeg.init

added theorem PrincipalSeg.init_iff

added theorem PrincipalSeg.irrefl

added def PrincipalSeg.ltEquiv

added def PrincipalSeg.ltLe

added theorem PrincipalSeg.lt_le_apply

added theorem PrincipalSeg.lt_le_top

added theorem PrincipalSeg.lt_top

added def PrincipalSeg.ofElement

added def PrincipalSeg.ofIsEmpty

added theorem PrincipalSeg.of_element_apply

added theorem PrincipalSeg.of_element_top

added theorem PrincipalSeg.of_is_empty_top

added def PrincipalSeg.pemptyToPunit

added theorem PrincipalSeg.topLtTop

added theorem PrincipalSeg.top_eq

added theorem PrincipalSeg.trans_apply

added theorem PrincipalSeg.trans_top

added structure PrincipalSeg

added theorem RelEmbedding.collapseF.lt

added theorem RelEmbedding.collapseF.not_lt

added theorem RelEmbedding.collapse_apply