Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2018-08-28 15:05 2b9c9a80

View on Github →

refactor(analysis): add nndist; add finite product of metric spaces; prepare for normed spaces

Estimated changes

Modified analysis/complex.lean

Modified analysis/ennreal.lean

deleted theorem topological_space.nhds_swap

deleted theorem topological_space.prod_mem_nhds_sets

deleted theorem topological_space.tendsto_nhds_generate_from

deleted theorem topological_space.tendsto_prod_mk_nhds

Modified analysis/metric_space.lean

added theorem coe_dist

deleted def dist

added theorem dist_pi_def

added theorem eq_of_nndist_eq_zero

added def nndist

added theorem nndist_comm

added theorem nndist_eq_zero

added theorem nndist_self

added theorem nndist_triangle

added theorem nndist_triangle_left

added theorem nndist_triangle_right

added theorem zero_eq_nndist

Modified analysis/nnreal.lean

Modified analysis/topology/continuity.lean

added theorem embedding.map_nhds_eq

added theorem nhds_swap

added theorem prod_mem_nhds_sets

added theorem tendsto_prod_mk_nhds

Modified analysis/topology/topological_space.lean

added theorem topological_space.tendsto_nhds_generate_from

Modified data/finset.lean

added theorem finset.image_const

modified theorem finset.inf_insert

modified theorem finset.inf_singleton

modified theorem finset.inf_union

added theorem finset.le_inf_iff

added theorem finset.max_singleton'

modified theorem finset.sup_insert

added theorem finset.sup_le_iff

modified theorem finset.sup_singleton

modified theorem finset.sup_union

Modified data/real/nnreal.lean

added theorem nnreal.bot_eq_zero

added theorem nnreal.mul_finset_sup

added theorem nnreal.mul_sup