English
The closure of the universal product in a product of groups equals the product of closures of the coordinate sets, provided each coordinate includes the identity.
Русский
Замыкание универсального произведения в произведении групп равно произведению замыканий координат, если каждая координата содержит тождественный элемент.
LaTeX
$$$\operatorname{closure}(\operatorname{univ}.\pi s) = \pi\,\operatorname{univ}(\operatorname{closure}(s(i)))$$$
Lean4
@[to_additive]
theorem closure_pi [Finite η] {s : Π i, Set (f i)} (hs : ∀ i, 1 ∈ s i) :
closure (univ.pi fun i => s i) = pi univ fun i => closure (s i) :=
le_antisymm ((closure_le _).2 <| pi_subset_pi_iff.2 <| .inl fun _ _ => subset_closure)
(by
classical
exact
pi_le_iff.mpr fun i =>
(gc_map_comap _).l_le <|
(closure_le _).2 fun _x hx =>
subset_closure <|
mem_univ_pi.mpr fun j => by
by_cases H : j = i
· subst H
simpa
· simpa [H] using hs _)
