Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2017-12-20 23:25 49a63b74

View on Github →

refactor(data/ordinal): rearrange files, more cofinality

Estimated changes

Modified algebra/linear_algebra/basic.lean

Modified analysis/real.lean

Modified analysis/topology/topological_space.lean

Modified analysis/topology/uniform_space.lean

Modified data/cardinal.lean

deleted theorem cardinal.embedding.antisymm

deleted def cardinal.embedding.arrow_congr_left

deleted def cardinal.embedding.arrow_congr_right

deleted theorem cardinal.embedding.coe_fn_mk

deleted theorem cardinal.embedding.inj'

deleted theorem cardinal.embedding.injective_min

deleted def cardinal.embedding.prod_congr

deleted theorem cardinal.embedding.refl_apply

deleted theorem cardinal.embedding.schroeder_bernstein

deleted def cardinal.embedding.sum_congr

deleted theorem cardinal.embedding.sum_congr_apply_inl

deleted theorem cardinal.embedding.sum_congr_apply_inr

deleted theorem cardinal.embedding.to_fun_eq_coe

deleted theorem cardinal.embedding.total

deleted theorem cardinal.embedding.trans_apply

deleted structure cardinal.embedding

added theorem cardinal.lift_down

added theorem cardinal.lt_omega

deleted theorem equiv.to_embedding_coe_fn

Modified data/ordinal.lean

deleted def empty_relation.is_well_order

deleted def is_irrefl.swap

deleted def is_irrefl_of_is_asymm

deleted def is_strict_order.swap

deleted def is_strict_total_order'.swap

deleted def is_strict_weak_order_of_is_order_connected

deleted def is_trans.swap

deleted def is_trichotomous.swap

deleted def order.preimage

deleted def order_embedding.cod_restrict

deleted theorem order_embedding.cod_restrict_apply

deleted theorem order_embedding.coe_fn_mk

deleted theorem order_embedding.coe_fn_to_embedding

deleted theorem order_embedding.eq_of_to_fun_eq

deleted theorem order_embedding.eq_preimage

deleted theorem order_embedding.nat_lt

deleted def order_embedding.of_monotone

deleted theorem order_embedding.of_monotone_coe

deleted theorem order_embedding.ord'

deleted def order_embedding.preimage

deleted theorem order_embedding.refl_apply

deleted def order_embedding.rsymm

deleted theorem order_embedding.trans_apply

deleted theorem order_embedding.well_founded_iff_no_descending_seq

deleted structure order_embedding

deleted theorem order_iso.apply_inverse_apply

deleted theorem order_iso.coe_coe_fn

deleted theorem order_iso.coe_fn_mk

deleted theorem order_iso.coe_fn_symm_mk

deleted theorem order_iso.coe_fn_to_equiv

deleted theorem order_iso.eq_of_to_fun_eq

deleted theorem order_iso.inverse_apply_apply

deleted def order_iso.of_surjective

deleted theorem order_iso.of_surjective_coe

deleted theorem order_iso.ord'

deleted def order_iso.preimage

deleted theorem order_iso.prod_lex_congr

deleted theorem order_iso.refl_apply

deleted theorem order_iso.sum_lex_congr

deleted theorem order_iso.trans_apply

deleted structure order_iso

modified theorem ordinal.card_omega

added theorem ordinal.cof_add

added theorem ordinal.cof_cof

added theorem ordinal.cof_eq

modified theorem ordinal.cof_eq_one_iff_is_succ

deleted theorem ordinal.exists_of_cof

added theorem ordinal.lift_card

added theorem ordinal.lift_is_limit

added theorem ordinal.lift_is_succ

added theorem ordinal.lift_pred

added theorem ordinal.lift_succ

added theorem ordinal.ord_cof_eq

added theorem ordinal.type_ne_zero_iff_nonempty

deleted def set_coe_embedding

deleted def subrel

deleted theorem well_founded.has_min

deleted def well_founded.min

deleted theorem well_founded.min_mem

deleted theorem well_founded.not_lt_min

Modified data/set/finite.lean

modified theorem set.finite_image

Modified data/sigma/basic.lean

modified theorem psigma.mk.inj_iff

added theorem subtype.coe_eta

added theorem subtype.coe_mk

Modified logic/basic.lean

added theorem Exists.fst

added theorem Exists.snd

Created logic/embedding.lean

added theorem equiv.to_embedding_coe_fn

added def function.embedding.arrow_congr_left

added def function.embedding.cod_restrict

added theorem function.embedding.cod_restrict_apply

added theorem function.embedding.coe_fn_mk

added theorem function.embedding.inj'

added def function.embedding.prod_congr

added theorem function.embedding.refl_apply

added def function.embedding.sum_congr

added theorem function.embedding.sum_congr_apply_inl

added theorem function.embedding.sum_congr_apply_inr

added theorem function.embedding.to_fun_eq_coe

added theorem function.embedding.trans_apply

added structure function.embedding

Modified logic/function.lean

modified def function.injective.decidable_eq

modified theorem function.injective.eq_iff

modified theorem function.injective_of_partial_inv

modified theorem function.injective_of_partial_inv_right

modified def function.is_partial_inv

modified theorem function.partial_inv_of_injective

modified theorem function.surj_inv_eq

Created logic/schroeder_bernstein.lean

added theorem function.embedding.antisymm

added theorem function.embedding.injective_min

added theorem function.embedding.schroeder_bernstein

added theorem function.embedding.total

Modified order/basic.lean

added def empty_relation.is_well_order

added def is_irrefl.swap

added def is_irrefl_of_is_asymm

added theorem is_order_connected.neg_trans

added def is_strict_order.swap

added def is_strict_total_order'.swap

added def is_strict_weak_order_of_is_order_connected

added def is_trans.swap

added def is_trichotomous.swap

added theorem well_founded.has_min

added theorem well_founded.min_mem

added theorem well_founded.not_lt_min

Modified order/filter.lean

Created order/order_iso.lean

added def order.preimage

added def order_embedding.cod_restrict

added theorem order_embedding.cod_restrict_apply

added theorem order_embedding.coe_fn_mk

added theorem order_embedding.coe_fn_to_embedding

added theorem order_embedding.eq_of_to_fun_eq

added theorem order_embedding.eq_preimage

added theorem order_embedding.nat_lt

added def order_embedding.of_monotone

added theorem order_embedding.of_monotone_coe

added theorem order_embedding.ord'

added def order_embedding.preimage

added theorem order_embedding.refl_apply

added def order_embedding.rsymm

added theorem order_embedding.trans_apply

added theorem order_embedding.well_founded_iff_no_descending_seq

added structure order_embedding

added theorem order_iso.apply_inverse_apply

added theorem order_iso.coe_coe_fn

added theorem order_iso.coe_fn_mk

added theorem order_iso.coe_fn_symm_mk

added theorem order_iso.coe_fn_to_equiv

added theorem order_iso.eq_of_to_fun_eq

added theorem order_iso.inverse_apply_apply

added theorem order_iso.of_surjective_coe

added theorem order_iso.ord'

added def order_iso.preimage

added theorem order_iso.prod_lex_congr

added theorem order_iso.refl_apply

added theorem order_iso.sum_lex_congr

added theorem order_iso.trans_apply

added structure order_iso

added def set_coe_embedding

added def subrel