English
If v factors through an embedding f into a normed field, the pseudo-metric space induced by v is the same as the pseudo-metric space induced by f.
Русский
Если v факторизуется через вложение f в нормированное поле, то псевдометрическое пространство, индуцированное v, совпадает с псевдометрическим пространством, индуцированным f.
LaTeX
$$$$\\mathrm{PseudoMetricSpace}(\\mathrm{induced\ } f) = (\\text{normedField}(v)).toPseudoMetricSpace.$$$$
Lean4
/-- If the absolute value `v` factors through an embedding `f` into a normed field, then
the pseudo metric space associated to the absolute value is the same as the pseudo metric space
induced by `f`. -/
theorem pseudoMetricSpace_induced_of_comp (h : ∀ x, ‖f x‖ = v x) :
PseudoMetricSpace.induced f inferInstance = (normedField v).toPseudoMetricSpace := by ext;
exact isometry_of_comp h |>.dist_eq _ _
