English
A preconnected set is contained in or disjoint from a closed cover by two closed sets.
Русский
Предсвязное множество содержится в или несовпадает с покрытием двумя замкнутыми множествами.
LaTeX
$$$IsPreconnected\ s \iff \forall u,v\ (IsClosed u \land IsClosed v) \to (s \subseteq u \cup v \to s \cap (u \cap v) = \emptyset \to s \subseteq u \lor s \subseteq v)$$$
Lean4
/-- A set `s` is preconnected if and only if
for every cover by two closed sets that are disjoint on `s`,
it is contained in one of the two covering sets. -/
theorem isPreconnected_iff_subset_of_disjoint_closed :
IsPreconnected s ↔ ∀ u v, IsClosed u → IsClosed v → s ⊆ u ∪ v → s ∩ (u ∩ v) = ∅ → s ⊆ u ∨ s ⊆ v :=
by
constructor <;> intro h
· intro u v hu hv hs huv
rw [isPreconnected_closed_iff] at h
specialize h u v hu hv hs
contrapose! huv
simp only [not_subset] at huv
rcases huv with ⟨⟨x, hxs, hxu⟩, ⟨y, hys, hyv⟩⟩
have hxv : x ∈ v := or_iff_not_imp_left.mp (hs hxs) hxu
have hyu : y ∈ u := or_iff_not_imp_right.mp (hs hys) hyv
exact h ⟨y, hys, hyu⟩ ⟨x, hxs, hxv⟩
· rw [isPreconnected_closed_iff]
intro u v hu hv hs hsu hsv
by_contra H
specialize h u v hu hv hs (Set.not_nonempty_iff_eq_empty.mp H)
apply H
rcases h with h | h
· rcases hsv with ⟨x, hxs, hxv⟩
exact ⟨x, hxs, ⟨h hxs, hxv⟩⟩
· rcases hsu with ⟨x, hxs, hxu⟩
exact ⟨x, hxs, ⟨hxu, h hxs⟩⟩
