connectedComponent_subset — Mathlib

English

If s is clopen and x ∈ s, then the connected component of x is contained in s.

Русский

Если s открыто и замкнуто, и x ∈ s, то связное компонента x ⊆ s.

LaTeX

$$$IsClopen s \to x \in s \to connectedComponent x \subseteq s$$$

Lean4

theorem connectedComponent_subset {x} (hs : IsClopen s) (hx : x ∈ s) : connectedComponent x ⊆ s :=
  isPreconnected_connectedComponent.subset_isClopen hs ⟨x, mem_connectedComponent, hx⟩

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