symm_bijective — Mathlib

English

Let e be an affine isometry equivalence between two normed affine spaces P and P₂. Then the inverse map e.symm is a bijection between P₂ and P.

Русский

Пусть e — аффинная изометрия-эквивалент между двумя нормированными афинными пространствами P и P₂. Тогда обратное отображение e.symm биективно отображает P₂ на P.

LaTeX

$$$\mathrm{Bijective}(\mathrm{AffineIsometryEquiv}.symm)$$$

Lean4

theorem symm_bijective : Bijective (AffineIsometryEquiv.symm : (P₂ ≃ᵃⁱ[𝕜] P) → _) :=
  Function.bijective_iff_has_inverse.mpr ⟨_, symm_symm, symm_symm⟩

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