English
If u and v are open and disjoint, and s ⊆ u ∪ v with (s ∩ u) nonempty and s preconnected, then s ⊆ u or s ⊆ v.
Русский
Пусть u и v открыты и попарно непересекаются; если s ⊆ u ∪ v и (s∩u)≠∅, и s предсвязно, тогда s ⊆ u или s ⊆ v.
LaTeX
$$$\\text{IsOpen}(u) \\land \\text{IsOpen}(v) \\land (u \\cap v = \\emptyset) \\land s \\subseteq u \\cup v \\land (s \\cap u) \\neq \\emptyset \\land \\mathrm{IsPreconnected}(s) \\Rightarrow s \\subseteq u \\lor s \\subseteq v$$$
Lean4
theorem preimage_of_isOpenMap [TopologicalSpace β] {s : Set β} (hs : IsConnected s) {f : α → β}
(hinj : Function.Injective f) (hf : IsOpenMap f) (hsf : s ⊆ range f) : IsConnected (f ⁻¹' s) :=
⟨hs.nonempty.preimage' hsf, hs.isPreconnected.preimage_of_isOpenMap hinj hf hsf⟩
