English
If each s(i) is preconnected, then the product over i of univ of s(i) is preconnected.
Русский
Если каждый s(i) предсвязно, тогда произведение по i множества s(i) предсвязно.
LaTeX
$$$\\forall i, \\mathrm{IsPreconnected}(s(i)) \\Rightarrow \\mathrm{IsPreconnected}(\\pi_{i} s(i))$$$
Lean4
/-- If a preconnected set `s` intersects an open set `u`, and limit points of `u` inside `s` are
contained in `u`, then the whole set `s` is contained in `u`. -/
theorem subset_of_closure_inter_subset (hs : IsPreconnected s) (hu : IsOpen u) (h'u : (s ∩ u).Nonempty)
(h : closure u ∩ s ⊆ u) : s ⊆ u :=
by
have A : s ⊆ u ∪ (closure u)ᶜ := by
intro x hx
by_cases xu : x ∈ u
· exact Or.inl xu
· right
intro h'x
exact xu (h (mem_inter h'x hx))
apply hs.subset_left_of_subset_union hu isClosed_closure.isOpen_compl _ A h'u
exact disjoint_compl_right.mono_right (compl_subset_compl.2 subset_closure)
