Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2017-12-08 08:32 bd013e80

View on Github →

feat(data/dardinal): wellordering of cardinals

Estimated changes

Modified algebra/linear_algebra/basic.lean

modified theorem exists_is_basis

added theorem exists_subset_is_basis

Modified analysis/measure_theory/measurable_space.lean

Modified analysis/metric_space.lean

Modified analysis/topology/topological_space.lean

Modified analysis/topology/topological_structures.lean

Modified data/bool.lean

added theorem bool.to_bool_coe

Modified data/cardinal.lean

added theorem cardinal.cantor

added theorem cardinal.le_iff_exists_add

added theorem cardinal.le_min

added theorem cardinal.le_sum

added theorem cardinal.le_sup

added def cardinal.min

added theorem cardinal.min_eq

added theorem cardinal.min_le

modified theorem cardinal.mul_power

added theorem cardinal.ne_zero_iff_nonempty

modified theorem cardinal.one_power

modified theorem cardinal.power_mono_left

modified theorem cardinal.power_mono_right

modified theorem cardinal.power_mul

modified theorem cardinal.power_sum

modified theorem cardinal.power_zero

added theorem cardinal.prop_eq_two

added def cardinal.sum

added def cardinal.sup

added theorem cardinal.sup_le

added theorem cardinal.zero_le

modified theorem cardinal.zero_power

deleted theorem embedding.exists_injective_or_surjective

added theorem embedding.injective_min

deleted def embedding.option.Sup

deleted theorem embedding.option.Sup_le

deleted theorem embedding.option.eq_of_le_some

deleted inductive embedding.option.le

deleted theorem embedding.option.le_Sup

deleted theorem embedding.option.mem_of_Sup_eq_some

deleted def embedding.option.strict_partial_order

deleted def embedding.pfun.partial_order

deleted def embedding.pfun

modified theorem embedding.total

Modified data/equiv.lean

Modified data/finset.lean

modified theorem finset.case_strong_induction_on

added theorem finset.le_iff_subset

added theorem finset.lt_iff_ssubset

modified theorem finset.strong_induction_on

added theorem finset.val_lt_iff

Modified data/multiset.lean

added theorem multiset.case_strong_induction_on

added theorem multiset.strong_induction_on

Modified data/set/basic.lean

added theorem set.empty_prod

added theorem set.eq_empty_iff_forall_not_mem

deleted theorem set.eq_empty_of_forall_not_mem

added theorem set.image_swap_eq_preimage_swap

added theorem set.image_swap_prod

added theorem set.insert_prod

modified theorem set.mem_insert_iff

added theorem set.mem_prod

added theorem set.mem_prod_eq

added theorem set.prod_empty

added theorem set.prod_image_image_eq

added theorem set.prod_insert

added theorem set.prod_inter_prod

added theorem set.prod_mk_mem_set_prod_eq

added theorem set.prod_mono

added theorem set.prod_neq_empty_iff

added theorem set.prod_preimage_eq

added theorem set.prod_singleton_singleton

added theorem set.univ_prod_univ

Modified data/set/default.lean

Modified data/set/disjointed.lean

Modified data/set/enumerate.lean

Modified data/set/finite.lean

Modified data/set/intervals.lean

Modified data/set/lattice.lean

deleted theorem bind_def

deleted theorem fmap_eq_image

deleted theorem image_Union

deleted theorem image_congr

deleted theorem mem_seq_iff

deleted theorem monotone_preimage

deleted theorem preimage_Union

deleted theorem preimage_sUnion

added theorem set.bind_def

added theorem set.fmap_eq_image

added theorem set.image_Union

added theorem set.image_congr

added theorem set.mem_seq_iff

added theorem set.monotone_preimage

added theorem set.monotone_prod

added theorem set.preimage_Union

added theorem set.preimage_sUnion

added theorem set.subtype_val_image

added theorem set.univ_subtype

deleted theorem subtype_val_image

deleted theorem univ_subtype

Deleted data/set/prod.lean

deleted theorem set.empty_prod

deleted theorem set.image_swap_eq_preimage_swap

deleted theorem set.image_swap_prod

deleted theorem set.insert_prod

deleted theorem set.mem_prod

deleted theorem set.mem_prod_eq

deleted theorem set.monotone_prod

deleted theorem set.prod_empty

deleted theorem set.prod_image_image_eq

deleted theorem set.prod_insert

deleted theorem set.prod_inter_prod

deleted theorem set.prod_mk_mem_set_prod_eq

deleted theorem set.prod_mono

deleted theorem set.prod_neq_empty_iff

deleted theorem set.prod_preimage_eq

deleted theorem set.prod_singleton_singleton

deleted theorem set.univ_prod_univ

Modified logic/basic.lean

added theorem empty.elim

Modified logic/function.lean

added theorem function.cantor_injective

added theorem function.cantor_surjective

Modified order/zorn.lean

added theorem zorn.chain.total

Modified theories/number_theory/dioph.lean

deleted def arity

deleted def curry

deleted def uncurry

added theorem vector3.append_add

deleted def vector3.append_add

added theorem vector3.append_cons

deleted def vector3.append_cons

added theorem vector3.append_left

deleted def vector3.append_left

added theorem vector3.append_nil

deleted def vector3.append_nil

added theorem vector3.cons_fs

deleted def vector3.cons_fs

added theorem vector3.cons_fz

deleted def vector3.cons_fz

added theorem vector3.insert_fs

deleted def vector3.insert_fs