iSup_map_mulSingle — Mathlib

English

A pair of equalities: the supremum over i of the image under mulSingle equals the full product Psi over univ; in particular, an explicit description of iSup of mapped submonoids.

Русский

Супремум изображений через mulSingle совпадает с полной проекцией на произведение.

LaTeX

$$iSup_map_mulSingle$$

Lean4

@[to_additive]
theorem iSup_map_mulSingle [DecidableEq ι] : ⨆ i, map (MonoidHom.mulSingle M i) (P i) = pi Set.univ P :=
  by
  haveI := Fintype.ofFinite ι
  refine iSup_map_mulSingle_le.antisymm fun x hx => ?_
  rw [← Finset.noncommProd_mul_single x]
  exact noncommProd_mem _ _ _ _ fun i _ => mem_iSup_of_mem _ (mem_map_of_mem _ (hx i trivial))

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