English
For finite index η and families H_i of subgroups of f_i, the subgroup pi univ H is contained in J iff each projection map from H_i to J is contained in J, i.e., the pi-embedding generates J in stages.
Русский
Для конечного индекса η и семейства подпогрупп H_i подпигруппы π_univ(H) ⊆ J эквивалентна тому, что каждая вложенная карта H_i → f_i образует подгруппу, вложенную в J.
LaTeX
$$$pi\, univ\, H \le J \iff \forall i,\; map (MonoidHom.mulSingle f i)(H_i) \le J$$$
Lean4
/-- For finite index types, the `Subgroup.pi` is generated by the embeddings of the groups. -/
@[to_additive /-- For finite index types, the `Subgroup.pi` is generated by the embeddings of the
additive groups. -/
]
theorem pi_le_iff [DecidableEq η] [Finite η] {H : ∀ i, Subgroup (f i)} {J : Subgroup (∀ i, f i)} :
pi univ H ≤ J ↔ ∀ i : η, map (MonoidHom.mulSingle f i) (H i) ≤ J :=
Submonoid.pi_le_iff
