apply_symm_apply — Mathlib

English

Let E be a nonempty affine subspace of P1', and φ an affine isometry P1'→P2. Then for x in E.map φ, φ((E.isometryEquivMap φ).symm x) = x.

Русский

Пусть E — непустое аффинное подпространство P1', φ — аффинная изометрия P1'→P2. Тогда для x ∈ E.map φ выполняется φ((E.isometryEquivMap φ).symm x) = x.

LaTeX

$$$\phi\bigl((E.isometryEquivMap \phi)^{-1}(x)\bigr) = x\quad \text{для } x \in E.map\phi.toAffineMap$$$

Lean4

@[simp]
theorem apply_symm_apply {E : AffineSubspace 𝕜 P₁'} [Nonempty E] {φ : P₁' →ᵃⁱ[𝕜] P₂} (x : E.map φ.toAffineMap) :
    φ ((E.isometryEquivMap φ).symm x) = x :=
  congr_arg Subtype.val <| (E.isometryEquivMap φ).apply_symm_apply _

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