iSup_map_mulSingle_le — Mathlib

English

The supremum over i of the image of S_i under map (mulSingle M i) is below the pi I S.

Русский

Наибольшая верхняя граница по i изображений S_i под отображением mulSingle меньше или равна π I S.

LaTeX

$$$ ⨆ i, map (MonoidHom.mulSingle M i) (S i) \le pi I S $$$

Lean4

@[to_additive]
theorem iSup_map_mulSingle_le [DecidableEq ι] {I : Set ι} {S : ∀ i, Submonoid (M i)} :
    ⨆ i, map (MonoidHom.mulSingle M i) (S i) ≤ pi I S :=
  iSup_le fun _ => map_le_iff_le_comap.mpr (le_comap_mulSingle_pi _)

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