map_iInf — Mathlib

English

Image preserves arbitrary infima: map f (iInf s) = ⨅ i, map f (s i).

Русский

Изображение сохраняет произвольные Inf: map f (iInf s) = ⨅ i, map f (s i).

LaTeX

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

Lean4

theorem map_iInf {ι : Sort*} [Nonempty ι] (f : F) (hf : Function.Injective f) (s : ι → NonUnitalSubsemiring R) :
    (map f (iInf s) : NonUnitalSubsemiring S) = ⨅ i, map f (s i) :=
  by
  apply SetLike.coe_injective
  simpa using (Set.injOn_of_injective hf).image_iInter_eq (s := SetLike.coe ∘ s)

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