Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2017-11-06 11:35 2bc7fd48

View on Github →

feat(data/cardinal): theory for cardinal arithmetic

Estimated changes

Created data/cardinal.lean

added theorem cardinal.add_mono

added theorem cardinal.mul_mono

added theorem cardinal.mul_power

added theorem cardinal.one_power

added theorem cardinal.power_mono_left

added theorem cardinal.power_mono_right

added theorem cardinal.power_mul

added theorem cardinal.power_sum

added theorem cardinal.power_zero

added theorem cardinal.zero_power

added def cardinal.ω

added def cardinal

added theorem embedding.antisymm

added def embedding.arrow_congr_left

added def embedding.arrow_congr_right

added theorem embedding.exists_injective_or_surjective

added def embedding.option.Sup

added theorem embedding.option.Sup_le

added theorem embedding.option.eq_of_le_some

added inductive embedding.option.le

added theorem embedding.option.le_Sup

added theorem embedding.option.mem_of_Sup_eq_some

added def embedding.option.strict_partial_order

added def embedding.pfun.partial_order

added def embedding.pfun

added def embedding.prod_congr

added theorem embedding.schroeder_bernstein

added def embedding.sum_congr

added theorem embedding.total

added structure embedding

added theorem equiv.of_bijective

Modified data/equiv.lean

added theorem equiv.arrow_empty_unit

added theorem equiv.empty_of_not_nonempty

Modified data/set/lattice.lean

added theorem image_congr