comap_supr — Mathlib

English

Let f be an affine map f: P1 → P2 and (s_i) be a family of affine subspaces of P2 indexed by i. Then the preimage of the infimum equals the infimum of the preimages: (iInf s).comap f = ⨅ i, (s i).comap f.

Русский

Пусть f — аффинное отображение P1 → P2 и {s_i} — семейство аффиновых подпространств P2, индексируемое i. Тогда предобразение наилучшего пересечения равно пересечению предобразий: (iInf s).comap f = ⨅ i, (s i).comap f.

LaTeX

$$$ (\\inf_i s_i).comap f = \\inf_i (s_i.comap f) $$$

Lean4

theorem comap_supr {ι : Sort*} (f : P₁ →ᵃ[k] P₂) (s : ι → AffineSubspace k P₂) :
    (iInf s).comap f = ⨅ i, (s i).comap f :=
  (gc_map_comap f).u_iInf

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