comap_iInf — Mathlib

English

Comap preserves arbitrary infima: comap f (iInf s) = iInf (comap f (s i)).

Русский

Комап сохраняет произвольные Inf: comap f (iInf s) = iInf (comap f (s i)).

LaTeX

$$$\\operatorname{comap}_f\\left(\\mathrm{iInf}_i s(i)\\right) = \\bigwedge_i \\operatorname{comap}_f\\left(s(i)\\right)$$$

Lean4

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

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