English
In a preconnected space, if s and t are open, s ∪ t = univ, and s and t are both nonempty, then s ∩ t is nonempty.
Русский
В предсвязанном пространстве, если s и t открыты, их объединение равно всей пространственной множеству, и они непусты, то пересечение s ∩ t непусто.
LaTeX
$$$[PreconnectedSpace\;\alpha]\;\{s,t:\;Set\;\alpha\} \to (IsOpen\ s) \to (IsOpen\ t) \to (s\cup t = \varnothing) \to s \neq \varnothing \to t \neq \varnothing \to (s \cap t) \neq \varnothing$$$
Lean4
theorem nonempty_inter [PreconnectedSpace α] {s t : Set α} :
IsOpen s → IsOpen t → s ∪ t = univ → s.Nonempty → t.Nonempty → (s ∩ t).Nonempty := by
simpa only [univ_inter, univ_subset_iff] using @PreconnectedSpace.isPreconnected_univ α _ _ s t
