English
If x ∈ s ∩ t and s,t are preconnected, then s ∪ t is preconnected.
Русский
Если x ∈ s ∩ t и s,t предсоединены, то s ∪ t предсоединено.
LaTeX
$$$$ x\\in s\\cap t\\;\\&\\; \\operatorname{IsPreconnected}(s) \\;\\&\\; \\operatorname{IsPreconnected}(t) \\Rightarrow \\operatorname{IsPreconnected}(s\\cup t). $$$$
Lean4
theorem union (x : α) {s t : Set α} (H1 : x ∈ s) (H2 : x ∈ t) (H3 : IsPreconnected s) (H4 : IsPreconnected t) :
IsPreconnected (s ∪ t) :=
sUnion_pair s t ▸
isPreconnected_sUnion x { s, t } (by rintro r (rfl | rfl | h) <;> assumption)
(by rintro r (rfl | rfl | h) <;> assumption)