toIsometryEquiv_injective — Mathlib

English

The map that sends a class of isometric maps to its associated isometric equivalence is injective.

Русский

Отображение, отправляющее класс изометрий в соответствующее изометрическое эквивалентное отображение, инъективно.

LaTeX

$$$\operatorname{Injective}\big((\uparrow): F \to \alpha \cong_i \beta\big)$$$

Lean4

theorem toIsometryEquiv_injective : Function.Injective ((↑) : F → α ≃ᵢ β) := fun _ _ e ↦
  DFunLike.ext _ _ fun a ↦ DFunLike.congr_fun e a

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