map_iInf — Mathlib

English

If f is injective, then the image of the infimum over an index set equals the infimum of the images: map f (iInf s) = iInf (map f s).

Русский

Если $f$ инъективно, образ пересечения по индексу равен пересечению образов: map f (iInf s) = iInf (map f s).

LaTeX

$$$\\mathrm{map}\\ f\\ (\\inf_i s(i)) = \\inf_i (\\mathrm{map}\\ f\\ (s(i)))$$$

Lean4

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

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