English
For finite η, the closure of the product of sets s_i equals the product of closures: closure(univ.π s) = π univ (closure s).
Русский
Для конечного η closure(π_i s_i) = π_i closure(s_i).
LaTeX
$$$[\text{Finite }\eta]\Rightarrow \operatorname{closure}\bigl(\operatorname{univ}.\pi (\lambda i, s_i)\bigr) = \pi\,\operatorname{univ}\, (\lambda i, 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 =>
map_le_of_le_comap _ <|
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 _)
