toHomeomorph_injective — Mathlib

English

The map taking a linear isometry equivalence to its homeomorph is injective: if two such equivalences yield the same homeomorph, they are equal.

Русский

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

LaTeX

$$$\mathrm{Injective}\big(\mathrm{toHomeomorph}: (E \simeq_{\mathrm{si}} E_2) \to E \simeq_t E_2\big)$$$

Lean4

theorem toHomeomorph_injective : Function.Injective (toHomeomorph : (E ≃ₛₗᵢ[σ₁₂] E₂) → E ≃ₜ E₂) := fun x _ h =>
  coe_injective (congr_arg _ h : ⇑x.toHomeomorph = _)

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