English
If v factors through an embedding f into a normed field L, then the uniform structure on WithAbs v is the pullback (comap) of the uniform structure on L via f.
Русский
Если v факторизуется через вложение f в нормированное поле L, то равенство униформных структур: UniformSpace.comap f (WithAbs v) = (normedField v).toUniformSpace.
LaTeX
$$$$UniformSpace.comap\\, f\\, \\mathrm{inferInstance} = (\\mathrm{normedField}(v)).toUniformSpace.$$$$
Lean4
/-- If the absolute value `v` factors through an embedding `f` into a normed field, then
the uniform structure associated to the absolute value is the same as the uniform structure
induced by `f`. -/
theorem uniformSpace_comap_eq_of_comp (h : ∀ x, ‖f x‖ = v x) :
UniformSpace.comap f inferInstance = (normedField v).toUniformSpace := by
simp only [← pseudoMetricSpace_induced_of_comp h, PseudoMetricSpace.toUniformSpace]
