English
If s is preconnected, and s ⊆ t ⊆ closure(s), then t is preconnected.
Русский
Если s предсвязно, и s ⊆ t ⊆ замыкание(s), то t предсвязно.
LaTeX
$$$\\mathrm{IsPreconnected}(s) \\land s \\subseteq t \\land t \\subseteq \\overline{s} \\Rightarrow \\mathrm{IsPreconnected}(t)$$$
Lean4
/-- Theorem of bark and tree: if a set is within a preconnected set and its closure, then it is
preconnected as well. See also `IsConnected.subset_closure`. -/
protected theorem subset_closure {s : Set α} {t : Set α} (H : IsPreconnected s) (Kst : s ⊆ t) (Ktcs : t ⊆ closure s) :
IsPreconnected t := fun u v hu hv htuv ⟨_y, hyt, hyu⟩ ⟨_z, hzt, hzv⟩ =>
let ⟨p, hpu, hps⟩ := mem_closure_iff.1 (Ktcs hyt) u hu hyu
let ⟨q, hqv, hqs⟩ := mem_closure_iff.1 (Ktcs hzt) v hv hzv
let ⟨r, hrs, hruv⟩ := H u v hu hv (Subset.trans Kst htuv) ⟨p, hps, hpu⟩ ⟨q, hqs, hqv⟩
⟨r, Kst hrs, hruv⟩
