Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2017-12-11 05:07 03074f19

View on Github →

feat(data/ordinal): more ordinals

Estimated changes

Modified data/bool.lean

Modified data/ordinal.lean

added def initial_seg.cod_restrict

added theorem initial_seg.cod_restrict_apply

added theorem initial_seg.coe_coe_fn

added def initial_seg.le_lt

added theorem initial_seg.le_lt_apply

added def initial_seg.lt_or_eq

added theorem initial_seg.lt_or_eq_apply_left

added theorem initial_seg.lt_or_eq_apply_right

added def order_embedding.cod_restrict

added theorem order_embedding.cod_restrict_apply

added def ordinal.enum

added theorem ordinal.enum_lt

added theorem ordinal.enum_type

added theorem ordinal.enum_typein

added theorem ordinal.induction_on

deleted def ordinal.le

added def ordinal.type

added theorem ordinal.type_def'

added theorem ordinal.type_def

added theorem ordinal.type_eq

added theorem ordinal.type_le

added theorem ordinal.type_lt

added def ordinal.typein

added theorem ordinal.typein_enum

added theorem ordinal.typein_inj

added theorem ordinal.typein_lt_type

added theorem ordinal.typein_lt_typein

added theorem ordinal.typein_surj

added theorem ordinal.typein_top

added theorem ordinal.wf

added def principal_seg.cod_restrict

added theorem principal_seg.cod_restrict_apply

added theorem principal_seg.cod_restrict_top

added theorem principal_seg.equiv_lt_top

deleted def principal_seg.le_lt

deleted theorem principal_seg.le_lt_apply

added theorem principal_seg.lt_le_top

added theorem principal_seg.lt_top

added def principal_seg.of_element

added theorem principal_seg.of_element_apply

added theorem principal_seg.of_element_top

added theorem principal_seg.top_eq

added theorem principal_seg.trans_top

modified def set_coe_embedding

added def subrel