Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2019-05-10 00:53 e66e1f30

View on Github →

feat(set_theory): add to cardinal, ordinal, cofinality (#963)

  • feat(set_theory): add to cardinal, ordinal, cofinality The main new fact is the infinite pigeonhole principle Also includes many basic additions
  • fix name change in other files
  • address all of Mario's comments
  • use classical tactic in order/basic I did not use it for well_founded.succ, because that resulted in an error in lt_succ
  • fix error

Estimated changes

added theorem not_bounded_iff
added theorem not_unbounded_iff
modified theorem well_founded.has_min
modified theorem well_founded.min_mem
modified theorem well_founded.not_lt_min
added theorem order_iso.ord''
added theorem cardinal.countable_iff
added theorem cardinal.le_powerlt
added theorem cardinal.mk_Union_le
added theorem cardinal.mk_bUnion_le
added theorem cardinal.mk_image_eq
added theorem cardinal.mk_range_eq
modified theorem cardinal.mk_range_le
added theorem cardinal.mk_sUnion_le
added theorem cardinal.mk_sep
added theorem cardinal.mk_set_le
added theorem cardinal.out_embedding
added theorem cardinal.powerlt_aux
added theorem cardinal.powerlt_le
added theorem cardinal.powerlt_max
added theorem cardinal.powerlt_succ
added theorem cardinal.powerlt_zero
added theorem cardinal.succ_ne_zero
added theorem cardinal.sup_eq_zero
added theorem cardinal.two_le_iff'
added theorem cardinal.two_le_iff
added theorem cardinal.zero_power_le
added theorem cardinal.zero_powerlt
modified def order.cof
added theorem order.cof_le
added theorem order.le_cof
added theorem ordinal.cof_type
added theorem ordinal.sup_lt
added theorem ordinal.sup_lt_ord
added def strict_order.cof
added theorem cardinal.add_one_eq
added theorem cardinal.mk_ord_out
added theorem cardinal.ord_injective
added theorem cardinal.power_nat_le
added theorem cardinal.powerlt_omega
added theorem ordinal.card_typein
added theorem ordinal.enum_le_enum
added theorem ordinal.mk_initial_seg
added theorem ordinal.order_iso_enum
added theorem ordinal.sup_succ
added theorem ordinal.type_out
added theorem ordinal.type_subrel_lt