map_iInf — Mathlib

English

Again, if f is injective, the image of an indexed infimum equals the indexed infimum of images: map f (iInf p_i) = iInf (map f p_i).

Русский

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

LaTeX

$$$\\operatorname{map}\\,f\\,\\bigl(i\\Inf_i p_i\\bigr) = i\\Inf_i (\\operatorname{map}\\,f\\,p_i)$$$

Lean4

theorem map_iInf {ι : Sort*} [Nonempty ι] {p : ι → Submodule R M} (f : F) (hf : Injective f) :
    (⨅ i, p i).map f = ⨅ i, (p i).map f :=
  SetLike.coe_injective <| by simpa only [map_coe, coe_iInf] using hf.injOn.image_iInter_eq

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