comap_span — Mathlib

English

Let f be an affine equivalence f: P1 ≃ᵃ[k] P2 and s a subset of P2. Then the preimage under f of the affine span of s equals the affine span of the preimage of s: (affineSpan k s).comap f = affineSpan k (f ⁻¹' s).

Русский

Пусть f — аффинное эквивалентное отображение P1 ≃ᵃ[k] P2 и s — множество в P2. Тогда предобразие по f афинного охвата s равно афинному охвату предобраза s: (affineSpan k s).comap f = affineSpan k (f ⁻¹' s).

LaTeX

$$$ (\\mathrm{affineSpan}\\ k\\ s).comap f = \\mathrm{affineSpan}\\ k (f^{-1}(s)) $$$

Lean4

theorem comap_span (f : P₁ ≃ᵃ[k] P₂) (s : Set P₂) : (affineSpan k s).comap (f : P₁ →ᵃ[k] P₂) = affineSpan k (f ⁻¹' s) :=
  by rw [← map_symm, map_span, AffineEquiv.coe_coe, f.image_symm]

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