map_symm — Mathlib

English

Let e be an affine equivalence and s an affine subspace of P2. Then the image of s under e.symm equals the preimage of s under e: s.map(e.symm) = s.comap e.

Русский

Пусть e — аффинное эквивалентное отображение и s — аффиновое подпространство P2. Тогда образ s через e.symm равен предобразу s через e: s.map(e.symm) = s.comap e.

LaTeX

$$$ s.map (e^{\\mathrm{symm}}) = s.comap e $$$

Lean4

@[simp]
theorem map_symm (e : P₁ ≃ᵃ[k] P₂) (s : AffineSubspace k P₂) : s.map (e.symm : P₂ →ᵃ[k] P₁) = s.comap e :=
  coe_injective <| e.image_symm _

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