map_iInf — Mathlib

English

For a family {S_i} of subsemigroups indexed by i in I, the image of their infimum under an injective map equals the infimum of the images.

Русский

Для семейства подполугрупп {S_i} индексированного по i ∈ I образ их инфимума под иньекции совпадает с инфимумом образов.

LaTeX

$$(iInf s).map f = iInf (fun i => (s i).map f)$$

Lean4

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

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