map_iInf — Mathlib

English

Let I be a nonempty index set and s: I → Subgroup G. Then (iInf s).map f = ⨅ i, (s(i)).map f for injective f.

Русский

Пусть I непусто и s: I → Subgroup G. Тогда (iInf s).map f = ⨅ i, (s(i)).map f при инъективном f.

LaTeX

$$$\\mathrm{map}_f\\Bigl(\\bigwedge_i s(i)\\Bigr) = \\bigwedge_i \\mathrm{map}_f(s(i))$ (при инъекции f).$$

Lean4

@[to_additive]
theorem map_iInf {ι : Sort*} [Nonempty ι] (f : G →* N) (hf : Function.Injective f) (s : ι → Subgroup G) :
    (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)

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