subset_closure — Mathlib

English

If s is connected and s ⊆ t ⊆ closure(s), then t is connected.

Русский

Если s связно, и s ⊆ t ⊆ closure(s), то t связано.

LaTeX

$$$\\mathrm{IsConnected}(s) \\Rightarrow s \\subseteq t \\Rightarrow t \\subseteq \\overline{s} \\Rightarrow \\mathrm{IsConnected}(t)$$$

Lean4

/-- Theorem of bark and tree: if a set is within a connected set and its closure, then it is
connected as well. See also `IsPreconnected.subset_closure`. -/
protected theorem subset_closure {s : Set α} {t : Set α} (H : IsConnected s) (Kst : s ⊆ t) (Ktcs : t ⊆ closure s) :
    IsConnected t :=
  ⟨Nonempty.mono Kst H.left, IsPreconnected.subset_closure H.right Kst Ktcs⟩

Похожие утверждения