Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2017-09-21 10:33 d9865aee

View on Github →

Merge branch 'master' of https://github.com/leanprover/mathlib

Estimated changes

Modified algebra/big_operators.lean

deleted theorem finset.abs_sum_le_sum_abs

deleted theorem finset.prod_sdiff

Modified algebra/field.lean

deleted theorem inv_pos

Modified algebra/group_power.lean

deleted theorem inv_inv'

deleted theorem inv_one

modified theorem pow_ge_one_of_ge_one

deleted theorem pow_inv

deleted theorem pow_le_pow

deleted theorem pow_ne_zero

deleted theorem pow_nonneg

modified theorem pow_pos

modified theorem pow_succ'

Modified algebra/ordered_monoid.lean

Modified data/finset/basic.lean

deleted theorem finset.exists_nat_subset_upto

deleted theorem finset.not_mem_upto

deleted theorem finset.sdiff_subset_sdiff

modified theorem finset.subset.refl

deleted theorem finset.upto_subset_upto_iff

modified theorem finset.upto_succ

modified theorem finset.upto_zero

deleted theorem lt_max_iff

Modified data/set/lattice.lean

deleted theorem set.sdiff_subset_sdiff

deleted theorem set.subset_Union

Modified order/boolean_algebra.lean

deleted theorem lattice.sub_le_sub

Modified topology/ennreal.lean

deleted theorem Inf_lt_iff

deleted theorem ennreal.le_of_forall_epsilon_le

deleted theorem ennreal.lt_add_right

deleted theorem ennreal.sum_of_real

deleted theorem ennreal.supr_add

deleted theorem infi_lt_iff

added theorem inv_inv'

added theorem inv_pos

Modified topology/infinite_sum.lean

deleted theorem add_div

deleted theorem filter.mem_at_top

deleted theorem has_sum_of_absolute_convergence

deleted theorem is_sum_iff_tendsto_nat_of_nonneg

deleted theorem tendsto_sum_nat_of_is_sum

Deleted topology/limits.lean

deleted theorem div_eq_mul_inv

deleted theorem exists_lt_of_nat

deleted theorem int_of_nat_eq_of_nat

deleted theorem is_sum_geometric

deleted theorem map_succ_at_top_eq

deleted theorem mul_add_one_le_pow

deleted theorem neg_inv

deleted def of_nat

deleted theorem of_nat_add

deleted theorem of_nat_bit0

deleted theorem of_nat_bit1

deleted theorem of_nat_le_of_nat

deleted theorem of_nat_le_of_nat_iff

deleted theorem of_nat_mul

deleted theorem of_nat_one

deleted theorem of_nat_sub

deleted theorem one_lt_inv

deleted theorem rat_coe_eq_of_nat

deleted theorem rat_of_nat_eq_of_nat

deleted theorem real_of_rat_of_nat_eq_of_nat

deleted theorem sum_geometric'

deleted theorem sum_geometric

deleted theorem tendsto_comp_succ_at_top_iff

deleted theorem tendsto_inverse_at_top_nhds_0

deleted theorem tendsto_pow_at_top_at_top_of_gt_1

deleted theorem tendsto_pow_at_top_nhds_0_of_lt_1

deleted theorem zero_le_of_nat

Modified topology/measure.lean

Modified topology/metric_space.lean

deleted theorem mem_uniformity_dist

Deleted topology/outer_measure.lean

deleted theorem Inter_neg

deleted theorem Inter_pos

deleted theorem Inter_univ

deleted theorem Union_empty

deleted theorem Union_neg

deleted theorem Union_pos

deleted theorem classical.or_not

deleted theorem ennreal.add_infi

deleted theorem ennreal.infi_add

deleted theorem ennreal.infi_add_infi

deleted theorem ennreal.infi_sum

deleted theorem inv_lt_one

deleted def measure_theory.outer_measure.inf

deleted theorem measure_theory.outer_measure.inf_space_is_measurable

deleted def measure_theory.outer_measure.measure

deleted def measure_theory.outer_measure.space

deleted theorem measure_theory.outer_measure.space_is_measurable_eq

deleted theorem measure_theory.outer_measure.subadditive

deleted structure measure_theory.outer_measure

deleted theorem sdiff_empty

deleted theorem sdiff_eq:

deleted theorem union_sdiff_left

deleted theorem union_sdiff_right

Modified topology/real.lean

modified theorem one_lt_two