Mathlib Changelog
v3
Changelog
About
Github
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