English
If any two points of a set S lie in some preconnected subset t ⊆ S, then S is preconnected.
Русский
Если любые две точки множества S лежат в некотором предсоединённом подмножества t ⊆ S, то S предсоединено.
LaTeX
$$$$ \\operatorname{IsPreconnected}(S) \\leftarrow \\forall x\\in S, \\forall y\\in S, \\exists t \\subseteq S, x\\in t \\wedge y\\in t \\wedge \\operatorname{IsPreconnected}(t). $$$$
Lean4
/-- If any two points of a set are contained in a preconnected subset,
then the original set is preconnected as well. -/
theorem isPreconnected_of_forall_pair {s : Set α}
(H : ∀ x ∈ s, ∀ y ∈ s, ∃ t, t ⊆ s ∧ x ∈ t ∧ y ∈ t ∧ IsPreconnected t) : IsPreconnected s :=
by
rcases eq_empty_or_nonempty s with (rfl | ⟨x, hx⟩)
exacts [isPreconnected_empty, isPreconnected_of_forall x fun y => H x hx y]
