isometryEquivOnRange — Mathlib

English

If f: α → β is an isometry, there exists an isometric bijection between α and range(f).

Русский

Если f: α → β является изометрией, существует изометрическое биекционное отображение между α и образом range(f).

LaTeX

$$$\exists e:\ α \cong_i \operatorname{range}(f)$$$

Lean4

/-- An isometry induces an isometric isomorphism between the source space and the
range of the isometry. -/
@[simps! +simpRhs toEquiv apply]
def isometryEquivOnRange [EMetricSpace α] [PseudoEMetricSpace β] {f : α → β} (h : Isometry f) : α ≃ᵢ range f
    where
  isometry_toFun := h
  toEquiv := Equiv.ofInjective f h.injective

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