map_sup — Mathlib

English

Let S and T be affine subspaces of an affine space P1, and let f be an affine map P1 → P2. Then the image of the join of S and T equals the join of their images: f(S ⊔ T) = f(S) ⊔ f(T).

Русский

Пусть S и T — аффиновые подпространства аффинного пространства P1, а f — аффинное отображение P1 в P2. Тогда образ объединения S и T равен объединению их образов: f(S ⊔ T) = f(S) ⊔ f(T).

LaTeX

$$$ f(S \\sqcup T) = f(S) \\sqcup f(T) $$$

Lean4

theorem map_sup (s t : AffineSubspace k P₁) (f : P₁ →ᵃ[k] P₂) : (s ⊔ t).map f = s.map f ⊔ t.map f :=
  (gc_map_comap f).l_sup

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