English
If for a set s there is a point x and every y ∈ s lies in some t ⊆ s with x ∈ t and y ∈ t, and each such t is preconnected, then s is preconnected.
Русский
Пусть для множества s существует точка x такая, что каждый y ∈ s принадлежит некоторому t ⊆ s, содержащему как x, так и y, и каждый такой t предсоединённо; тогда s предсоединено.
LaTeX
$$$$ \\forall x \\in \\alpha,\\ \\bigl(\\forall y \\in S,\\ \\exists t \\subseteq S,\\ x \\in t \\wedge y \\in t \\wedge \\operatorname{IsPreconnected}(t)\\bigr) \\Rightarrow \\operatorname{IsPreconnected}(S). $$$$
Lean4
/-- If any point of a set is joined to a fixed point by a preconnected subset,
then the original set is preconnected as well. -/
theorem isPreconnected_of_forall {s : Set α} (x : α) (H : ∀ y ∈ s, ∃ t, t ⊆ s ∧ x ∈ t ∧ y ∈ t ∧ IsPreconnected t) :
IsPreconnected s := by
rintro u v hu hv hs ⟨z, zs, zu⟩ ⟨y, ys, yv⟩
have xs : x ∈ s := by
rcases H y ys with ⟨t, ts, xt, -, -⟩
exact ts xt
cases hs xs with
| inl xu =>
rcases H y ys with ⟨t, ts, xt, yt, ht⟩
have := ht u v hu hv (ts.trans hs) ⟨x, xt, xu⟩ ⟨y, yt, yv⟩
exact this.imp fun z hz => ⟨ts hz.1, hz.2⟩
| inr xv =>
rcases H z zs with ⟨t, ts, xt, zt, ht⟩
have := ht v u hv hu (ts.trans <| by rwa [union_comm]) ⟨x, xt, xv⟩ ⟨z, zt, zu⟩
exact this.imp fun _ h => ⟨ts h.1, h.2.2, h.2.1⟩
