English
For finite η, with H(i) ⊆ Submonoid f i and J a Submonoid of the product, the inclusion pi univ H ≤ J holds if and only if for every i, the image of H(i) under the i-th embedding lies inside J.
Русский
Для конечного множества индексов η: включение pi univ H ≤ J эквивалентно тому, что для каждого i образ H(i) при i-ой встраивании лежит в J.
LaTeX
$$$[\text{Finite }\eta] \Rightarrow (\pi univ\ H \le J) \Leftrightarrow (\forall i : \eta,\ map (MonoidHom.mulSingle f i) (H i) \le J)$$$
Lean4
/-- For finite index types, the `Submonoid.pi` is generated by the embeddings of the monoids. -/
@[to_additive /-- For finite index types, the `Submonoid.pi` is generated by the embeddings of the
additive monoids. -/
]
theorem pi_le_iff [Finite η] [DecidableEq η] {H : Π i, Submonoid (f i)} {J : Submonoid (Π i, f i)} :
pi univ H ≤ J ↔ ∀ i : η, map (MonoidHom.mulSingle f i) (H i) ≤ J :=
⟨fun h i _ ⟨x, hx, H⟩ => h <| by simpa [← H], fun h x hx =>
pi_mem_of_mulSingle_mem x fun i => h i (mem_map_of_mem _ (hx i trivial))⟩
