Commit 2021-04-13 23:14 724f804b

View on Github →

refactor(src/analysis/normed_space/linear_isometry): generalize to semi_normed_group (#7122) This is part of a series of PR to include the theory of seminormed things in mathlib.

Estimated changes

Modified src/analysis/normed_space/linear_isometry.lean

modified theorem linear_isometry.map_eq_iff

modified theorem linear_isometry.map_ne

modified structure linear_isometry

modified structure linear_isometry_equiv

Modified src/data/complex/is_R_or_C.lean

modified theorem is_R_or_C.conj_clm_norm

Modified src/data/padics/padic_integers.lean

Modified src/measure_theory/set_integral.lean

Modified src/topology/metric_space/antilipschitz.lean

added theorem antilipschitz_with.comap_uniformity_le

added theorem antilipschitz_with.is_closed_range

added theorem antilipschitz_with.is_complete_range

deleted theorem antilipschitz_with.uniform_embedding

deleted theorem antilipschitz_with.uniform_embedding_of_injective

Modified src/topology/metric_space/closeds.lean

Modified src/topology/metric_space/isometry.lean

modified theorem isometry.comp_continuous_iff

modified theorem isometry.comp_continuous_on_iff

added theorem isometry.uniform_inducing

Modified src/topology/metric_space/pi_Lp.lean

Modified src/topology/uniform_space/basic.lean

added theorem to_nhds_mono

Modified src/topology/uniform_space/uniform_embedding.lean

modified theorem complete_space_iff_is_complete_range

modified theorem is_complete_image_iff

added theorem uniform_inducing.is_complete_range