Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2018-01-06 18:57 182c3035

View on Github →

feat(set_theory/cofinality): regular/inaccessible cards, Konig's theorem, next fixpoint function

Estimated changes

Modified algebra/functions.lean

added theorem abs_one

Modified data/equiv.lean

added def equiv.Pi_congr_right

Modified logic/embedding.lean

added def function.embedding.Pi_congr_right

added def function.embedding.sigma_congr_right

Modified logic/function.lean

added theorem function.inv_fun_surjective

Modified set_theory/cardinal.lean

added theorem cardinal.add_def

added theorem cardinal.cantor'

added theorem cardinal.lift_id'

modified theorem cardinal.lift_id

added theorem cardinal.lift_succ

added theorem cardinal.lift_two_power

added theorem cardinal.lt_succ

added theorem cardinal.mk_out

added theorem cardinal.mul_def

added theorem cardinal.omega_pos

added theorem cardinal.one_le_iff_ne_zero

added theorem cardinal.one_le_iff_pos

added theorem cardinal.pos_iff_ne_zero

added theorem cardinal.power_def

added theorem cardinal.power_ne_zero

added def cardinal.prod

added theorem cardinal.prod_const

added theorem cardinal.prod_eq_zero

added theorem cardinal.prod_le_prod

added theorem cardinal.prod_mk

added theorem cardinal.prod_ne_zero

modified def cardinal.sum

added theorem cardinal.sum_const

added theorem cardinal.sum_le_sum

added theorem cardinal.sum_le_sup

added theorem cardinal.sum_lt_prod

added theorem cardinal.sum_mk

added theorem cardinal.sup_le_sum

added theorem cardinal.sup_le_sup

Created set_theory/cofinality.lean

added theorem cardinal.cof_is_regular

added theorem cardinal.is_inaccessible.mk

added def cardinal.is_inaccessible

added def cardinal.is_limit

added def cardinal.is_regular

added theorem cardinal.is_strong_limit.is_limit

added def cardinal.is_strong_limit

added theorem cardinal.lt_cof_power

added theorem cardinal.lt_power_cof

added theorem cardinal.omega_is_regular

added theorem cardinal.succ_is_regular

added theorem cardinal.univ_inaccessible

added def order.cof

added theorem order_iso.cof.aux

added theorem order_iso.cof

added def ordinal.cof

added theorem ordinal.cof_add

added theorem ordinal.cof_bsup_le

added theorem ordinal.cof_bsup_le_lift

added theorem ordinal.cof_cof

added theorem ordinal.cof_eq'

added theorem ordinal.cof_eq

added theorem ordinal.cof_eq_one_iff_is_succ

added theorem ordinal.cof_eq_zero

added theorem ordinal.cof_le_card

added theorem ordinal.cof_omega

added theorem ordinal.cof_ord_le

added theorem ordinal.cof_succ

added theorem ordinal.cof_sup_le

added theorem ordinal.cof_sup_le_lift

added theorem ordinal.cof_type_le

added theorem ordinal.cof_univ

added theorem ordinal.cof_zero

added theorem ordinal.le_cof_type

added theorem ordinal.lift_cof

added theorem ordinal.lt_cof_type

added theorem ordinal.omega_le_cof

added theorem ordinal.ord_cof_eq

Modified set_theory/ordinal.lean

added theorem cardinal.lift_lt_univ'

added theorem cardinal.lift_lt_univ

added theorem cardinal.lift_univ

added theorem cardinal.lt_univ'

added theorem cardinal.lt_univ

added theorem cardinal.mk_cardinal

added theorem cardinal.ord_univ

added theorem cardinal.type_cardinal

added def cardinal.univ

added theorem cardinal.univ_id

added theorem cardinal.univ_umax

deleted def cof

deleted def order.cof

deleted theorem order_iso.cof.aux

deleted theorem order_iso.cof

added theorem ordinal.card_univ

deleted theorem ordinal.cof_add

deleted theorem ordinal.cof_bsup_le

deleted theorem ordinal.cof_bsup_le_lift

deleted theorem ordinal.cof_cof

deleted theorem ordinal.cof_eq

deleted theorem ordinal.cof_eq_one_iff_is_succ

deleted theorem ordinal.cof_eq_zero

deleted theorem ordinal.cof_le_card

deleted theorem ordinal.cof_succ

deleted theorem ordinal.cof_sup_le

deleted theorem ordinal.cof_sup_le_lift

deleted theorem ordinal.cof_type_le

deleted theorem ordinal.cof_zero

added def ordinal.deriv

added theorem ordinal.deriv_is_normal

added theorem ordinal.deriv_limit

added theorem ordinal.deriv_succ

added theorem ordinal.deriv_zero

added theorem ordinal.foldr_le_nfp

added theorem ordinal.is_normal.bsup

added theorem ordinal.is_normal.deriv_fp

added theorem ordinal.is_normal.fp_iff_deriv

added theorem ordinal.is_normal.le_nfp

added theorem ordinal.is_normal.lt_nfp

added theorem ordinal.is_normal.nfp_fp

added theorem ordinal.is_normal.nfp_le

added theorem ordinal.is_normal.nfp_le_fp

added theorem ordinal.is_normal.sup

deleted theorem ordinal.le_cof_type

added theorem ordinal.le_nfp_self

modified theorem ordinal.lift.principal_seg_top

added theorem ordinal.lift_id'

modified theorem ordinal.lift_id

added theorem ordinal.lift_type

added theorem ordinal.lift_univ

deleted theorem ordinal.lt_cof_type

added theorem ordinal.lt_sup

added def ordinal.nfp

added theorem ordinal.not_zero_is_limit

deleted theorem ordinal.ord_cof_eq

added def ordinal.univ

added theorem ordinal.univ_id

added theorem ordinal.univ_umax

Modified set_theory/ordinal_notation.lean