comap_inf — Mathlib

English

For affine subspaces S and T of P2 and an affine map f: P1 → P2, the preimage of the intersection equals the intersection of the preimages: (S ∩ T).comap f = S.comap f ∩ T.comap f.

Русский

Для аффиновых подпространств S и T пространства P2 и аффинного отображения f: P1 → P2 выполняется: предобразие пересечения равно пересечению предобразий: (S ∩ T).comap f = S.comap f ∩ T.comap f.

LaTeX

$$$ (S \\cap T)^{{\\mathrm{comap} f}} = S^{{\\mathrm{comap} f}} \\cap T^{{\\mathrm{comap} f}} $$$

Lean4

theorem comap_inf (s t : AffineSubspace k P₂) (f : P₁ →ᵃ[k] P₂) : (s ⊓ t).comap f = s.comap f ⊓ t.comap f :=
  (gc_map_comap f).u_inf

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