Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2018-11-09 10:22 6273837f

View on Github →

feat(analysis): add emetric spaces

Estimated changes

Modified algebra/ordered_ring.lean

added theorem with_top.coe_nat

added theorem with_top.nat_ne_top

added theorem with_top.top_ne_nat

Created analysis/emetric_space.lean

added theorem emetric_space.cauchy_of_emetric

added theorem emetric_space.edist_eq_zero

added theorem emetric_space.edist_mem_uniformity

added theorem emetric_space.edist_triangle_left

added theorem emetric_space.edist_triangle_right

added theorem emetric_space.eq_of_forall_edist_le

added def emetric_space.induced

added theorem emetric_space.induced_uniform_embedding

added theorem emetric_space.mem_uniformity_edist

added def emetric_space.replace_uniformity

added theorem emetric_space.subtype.edist_eq

added theorem emetric_space.uniform_continuous_of_emetric

added theorem emetric_space.uniform_embedding_of_emetric

added def emetric_space.uniform_space_of_edist

added theorem emetric_space.uniformity_edist''

added theorem emetric_space.uniformity_edist'

added theorem emetric_space.zero_eq_edist

added theorem uniformity_dist_of_mem_uniformity

Modified analysis/ennreal.lean

Modified analysis/metric_space.lean

deleted theorem coe_dist

added theorem dist_eq_edist

added theorem dist_eq_nndist

added theorem edist_dist

added theorem edist_eq_dist

added theorem edist_eq_nndist

added theorem edist_ne_top

added theorem mem_uniformity_dist_edist

added theorem nndist_eq_dist

added theorem nndist_eq_edist

deleted theorem uniformity_dist_of_mem_uniformity

added theorem uniformity_edist'

added theorem uniformity_edist

Modified data/complex/exponential.lean

Modified data/finset.lean

added theorem finset.comp_inf_eq_inf_comp

added theorem finset.comp_sup_eq_sup_comp

added theorem finset.lt_inf

added theorem finset.sup_lt

Modified data/nat/cast.lean

modified theorem nat.cast_pos

Modified data/real/basic.lean

Modified data/real/cau_seq_filter.lean

Modified data/real/ennreal.lean

added theorem ennreal.add_halves

added theorem ennreal.add_lt_add

added theorem ennreal.coe_div

modified theorem ennreal.coe_nat

added theorem ennreal.div_add_div_same

added theorem ennreal.div_pos_iff

added theorem ennreal.div_self

added theorem ennreal.nat_ne_top

added theorem ennreal.to_nnreal_eq_zero_iff

added theorem ennreal.top_ne_nat

added theorem ennreal.zero_to_nnreal

Modified data/real/nnreal.lean

added theorem nnreal.add_halves

added theorem nnreal.div_add_div_same

added theorem nnreal.of_real_eq_zero

Modified order/bounded_lattice.lean

added theorem lattice.bot_lt_iff_ne_bot

added theorem lattice.lt_top_iff_ne_top