map_iSup — Mathlib

English

Let f be an affine map f: P1 → P2 and let (s_i) be a family of affine subspaces of P1 indexed by i. Then the image under f of the supremum of the family equals the supremum of the images: (iSup s).map f = ⨆ i, (s i).map f.

Русский

Пусть f — аффинное отображение P1 в P2, и пусть {s_i} — семейство аффиновых подпространств P1, индексируемое i. Тогда образ над этим семейством равен верхнему объединению образов: (iSup s).map f = ⨆ i, (s i).map f.

LaTeX

$$$ (\\mathrm{iSup}\\, s).map f = \\;\\big\\vee_i (s(i).map f) $$$

Lean4

theorem map_iSup {ι : Sort*} (f : P₁ →ᵃ[k] P₂) (s : ι → AffineSubspace k P₁) : (iSup s).map f = ⨆ i, (s i).map f :=
  (gc_map_comap f).l_iSup

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