isometry_induced — Mathlib

English

Let f: α → β be a function and suppose β is a metric space. If α is equipped with the metric induced by f via an injection hf, then f is an isometry from (α, d_α) to (β, d_β), i.e., d_β(f(x), f(y)) = d_α(x,y) for all x,y ∈ α with d_α(x,y) = d_β(f(x), f(y)).

Русский

Пусть f: α → β — функция, β — метрическое пространство. При наделении α метрикой, индуцированной по f через hf, выполняется, что f является изометрией между (α, d_α) и (β, d_β): d_β(f(x), f(y)) = d_α(x,y).

LaTeX

$$$ \forall x,y \in \alpha:\; d_\beta(f(x), f(y)) = d_\alpha(x,y), \; d_\alpha(x,y) := d_\beta(f(x), f(y)). $$$

Lean4

theorem isometry_induced (f : α → β) (hf : f.Injective) [m : MetricSpace β] :
    letI := m.induced f hf;
    Isometry f :=
  fun _ _ ↦ rfl

Похожие утверждения