English
If s is preconnected and s ⊆ u ∪ v with u,v open, then s ⊆ u or s ⊆ v.
Русский
Если s предсвязно и s ⊆ u ∪ v с открытыми u, v, то s ⊆ u или s ⊆ v.
LaTeX
$$$\\text{IsOpen}(u) \\land \\text{IsOpen}(v) \\land s \\subseteq u \\cup v \\land \\mathrm{IsPreconnected}(s) \\Rightarrow s \\subseteq u$$$
Lean4
theorem subset_or_subset (hu : IsOpen u) (hv : IsOpen v) (huv : Disjoint u v) (hsuv : s ⊆ u ∪ v)
(hs : IsPreconnected s) : s ⊆ u ∨ s ⊆ v :=
by
specialize hs u v hu hv hsuv
obtain hsu | hsu := (s ∩ u).eq_empty_or_nonempty
· exact Or.inr ((Set.disjoint_iff_inter_eq_empty.2 hsu).subset_right_of_subset_union hsuv)
· replace hs := mt (hs hsu)
simp_rw [Set.not_nonempty_iff_eq_empty, ← Set.disjoint_iff_inter_eq_empty, disjoint_iff_inter_eq_empty.1 huv] at hs
exact Or.inl ((hs s.disjoint_empty).subset_left_of_subset_union hsuv)
