Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2018-01-19 17:05 baa4b09e

View on Github →

feat(analysis/real): swap out the definition of real, shorten proofs

Estimated changes

Modified analysis/ennreal.lean

Modified analysis/limits.lean

Modified analysis/measure_theory/borel_space.lean

Modified analysis/measure_theory/lebesgue_measure.lean

Modified analysis/metric_space.lean

Modified analysis/real.lean

deleted theorem abs_real_eq_abs

deleted theorem closure_of_rat_image_le_eq

deleted theorem closure_of_rat_image_le_le_eq

added theorem closure_of_rat_image_lt

deleted theorem coe_rat_eq_of_rat

modified theorem compact_ivl

deleted theorem continuous_abs_rat

deleted theorem continuous_abs_real

deleted theorem continuous_inv_real'

deleted theorem continuous_inv_real

deleted theorem continuous_mul_real'

deleted theorem continuous_mul_real

added theorem continuous_of_rat

modified theorem dense_embedding_of_rat

deleted theorem dense_embedding_of_rat_of_rat

added theorem embedding_of_rat

deleted theorem exists_gt_of_rat

deleted theorem exists_lt_nat

deleted theorem exists_lt_of_rat

deleted theorem exists_lt_rat

deleted theorem exists_pos_of_rat

deleted theorem exists_rat_btwn

deleted theorem exists_rat_lt

deleted def lift_rat_fun

deleted theorem lift_rat_fun_of_rat

deleted def lift_rat_op

deleted theorem lift_rat_op_of_rat_of_rat

deleted theorem map_neg_rat

deleted theorem map_neg_real

deleted theorem max_of_rat

deleted theorem mem_nonneg_of_continuous2

deleted theorem mem_uniformity_rat

deleted theorem mem_uniformity_real_iff

deleted theorem mem_zero_nhd

deleted theorem mem_zero_nhd_iff

deleted theorem mem_zero_nhd_le

deleted theorem min_of_rat

deleted theorem nhds_0_eq_zero_nhd

deleted theorem nhds_eq_map_zero_nhd

deleted theorem nhds_eq_real

deleted def nonneg

deleted theorem nonneg_antisymm

deleted def of_rat

deleted theorem of_rat_abs

deleted theorem of_rat_add

deleted theorem of_rat_inj

deleted theorem of_rat_injective

deleted theorem of_rat_inv

deleted theorem of_rat_le

deleted theorem of_rat_lt

deleted theorem of_rat_mem_nonneg

deleted theorem of_rat_mem_nonneg_iff

deleted theorem of_rat_mul

deleted theorem of_rat_neg

deleted theorem of_rat_one

deleted theorem of_rat_sub

deleted theorem of_rat_zero

deleted theorem preimage_neg_rat

deleted theorem pure_zero_le_zero_nhd

added theorem rat.continuous_abs

added theorem rat.continuous_mul

added theorem rat.dist_eq

added theorem rat.totally_bounded_Icc

added theorem rat.uniform_continuous_abs

added theorem rat.uniform_continuous_add

added theorem rat.uniform_continuous_neg

added theorem real.Cauchy_eq

added theorem real.Ioo_eq_ball

added theorem real.ball_eq_Ioo

added theorem real.continuous_abs

added theorem real.continuous_inv'

added theorem real.continuous_inv

added theorem real.continuous_mul

deleted theorem real.le_def

deleted theorem real.neg_preimage_closure

added theorem real.tendsto_inv

added theorem real.totally_bounded_Icc

added theorem real.totally_bounded_Ico

added theorem real.totally_bounded_Ioo

added theorem real.totally_bounded_ball

added theorem real.uniform_continuous_abs

added theorem real.uniform_continuous_add

added theorem real.uniform_continuous_inv

added theorem real.uniform_continuous_mul

added theorem real.uniform_continuous_mul_const

added theorem real.uniform_continuous_neg

deleted def real

deleted theorem tendsto_add_rat_zero'

deleted theorem tendsto_add_rat_zero

deleted theorem tendsto_inv_pos_rat

deleted theorem tendsto_inv_rat

deleted theorem tendsto_inv_real

deleted theorem tendsto_mul_bnd_rat'

deleted theorem tendsto_mul_bnd_rat

deleted theorem tendsto_mul_rat'

deleted theorem tendsto_neg_rat_zero

deleted theorem tendsto_sub_rat'

deleted theorem tendsto_sub_uniformity_zero_nhd'

deleted theorem tendsto_sub_uniformity_zero_nhd

deleted theorem tendsto_zero_nhds

deleted theorem totally_bounded_01_rat

deleted theorem two_eq_of_rat_two

deleted theorem uniform_continuous_abs_rat

deleted theorem uniform_continuous_abs_real

deleted theorem uniform_continuous_add_rat

deleted theorem uniform_continuous_add_real

deleted theorem uniform_continuous_inv_pos_rat

deleted theorem uniform_continuous_mul_rat

deleted theorem uniform_continuous_neg_rat

deleted theorem uniform_continuous_neg_real

added theorem uniform_continuous_of_rat

deleted theorem uniform_continuous_rat'

deleted theorem uniform_continuous_rat

deleted theorem uniform_embedding_add_rat

deleted theorem uniform_embedding_mul_rat

modified theorem uniform_embedding_of_rat

deleted theorem uniformity_rat

deleted theorem zero_le_iff_nonneg

deleted def zero_nhd

Modified analysis/topology/topological_structures.lean

modified theorem is_closed_ge'

modified theorem is_closed_le'

Renamed analysis/complex.lean to data/complex.lean