comap_symm — Mathlib

English

Let e be an affine equivalence between P1 and P2, and s an affine subspace of P2. Then pulling back s by the inverse map equals the image of s under e: s.comap (e.symm) = s.map e.

Русский

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

LaTeX

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

Lean4

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

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