English
The underlying set of pi I H equals Set.pi I (H i as sets).
Русский
Множество подстановки pi I H равно множества Set.pi I (H i как множества).
LaTeX
$$$ (\mathrm{pi} I H : \mathrm{Set}(\Pi i, f i)) = \mathrm{Set.pi} I \bigl(\lambda i, (H i : \mathrm{Set}(f i))\bigr) $$$
Lean4
/-- A version of `Set.pi` for subgroups. Given an index set `I` and a family of submodules
`s : Π i, Subgroup f i`, `pi I s` is the subgroup of dependent functions `f : Π i, f i` such that
`f i` belongs to `pi I s` whenever `i ∈ I`. -/
@[to_additive /-- A version of `Set.pi` for `AddSubgroup`s. Given an index set `I` and a family
of submodules `s : Π i, AddSubgroup f i`, `pi I s` is the `AddSubgroup` of dependent functions
`f : Π i, f i` such that `f i` belongs to `pi I s` whenever `i ∈ I`. -/
]
def pi (I : Set η) (H : ∀ i, Subgroup (f i)) : Subgroup (∀ i, f i) :=
{ Submonoid.pi I fun i => (H i).toSubmonoid with inv_mem' := fun hp i hI => (H i).inv_mem (hp i hI) }
