English
A closed set is preconnected iff for every finite disjoint closed cover of it the cover forces a split into one side.
Русский
Замкнутое множество является предсвязанным тогда и только тогда, когда для любого конечного раздельного замкнутого покрытия его можно свести к одной стороне покрытия.
LaTeX
$$$IsPreconnected s \iff \forall u,v (IsClosed u \land IsClosed v) \to s \subseteq u \cup v \to Disjoint u v \to s \subseteq u \lor s \subseteq v$$$
Lean4
/-- A closed set `s` is preconnected if and only if for every cover by two closed sets that are
disjoint, it is contained in one of the two covering sets. -/
theorem isPreconnected_iff_subset_of_fully_disjoint_closed {s : Set α} (hs : IsClosed s) :
IsPreconnected s ↔ ∀ u v, IsClosed u → IsClosed v → s ⊆ u ∪ v → Disjoint u v → s ⊆ u ∨ s ⊆ v :=
by
refine isPreconnected_iff_subset_of_disjoint_closed.trans ⟨?_, ?_⟩ <;> intro H u v hu hv hss huv
· apply H u v hu hv hss
rw [huv.inter_eq, inter_empty]
have H1 := H (u ∩ s) (v ∩ s)
rw [subset_inter_iff, subset_inter_iff] at H1
simp only [Subset.refl, and_true] at H1
apply H1 (hu.inter hs) (hv.inter hs)
· rw [← union_inter_distrib_right]
exact subset_inter hss Subset.rfl
· rwa [disjoint_iff_inter_eq_empty, ← inter_inter_distrib_right, inter_comm]
