comap_iInf — Mathlib

English

Let s: ι → NonUnitalSubring S be a family. Then the comap of the infimum equals the infimum of the comaps: (iInf s).comap f = ⨅ i, (s i).comap f.

Русский

Для семейства s_i подполь в S верно: прообраз пересечения равен пересечению прообразов: (iInf s).comap f = ⨅ i, (s i).comap f.

LaTeX

$$$(\iInf s).comap f = \bigwedge_{i} (s(i)).comap f$$$

Lean4

theorem comap_iInf {ι : Sort*} (f : F) (s : ι → NonUnitalSubring S) : (iInf s).comap f = ⨅ i, (s i).comap f :=
  (gc_map_comap f).u_iInf

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