subset_isClopen — Mathlib

English

A preconnected set is contained in or disjoint from any given clopen set when their intersection is nonempty.

Русский

Предсвязанное множество содержится в любом открытом и замкнутом множестве или разобщено с ним, если их пересечение несовпусто.

LaTeX

$$$$\\text{IsPreconnected}(s) \\land \\text{IsClopen}(t) \\land (s \\cap t).\\mathrm{Nonempty} \\Rightarrow s \\subseteq t$$$$

Lean4

/-- Preconnected sets are either contained in or disjoint to any given clopen set. -/
theorem subset_isClopen {s t : Set α} (hs : IsPreconnected s) (ht : IsClopen t) (hne : (s ∩ t).Nonempty) : s ⊆ t :=
  hs.subset_left_of_subset_union ht.isOpen ht.compl.isOpen disjoint_compl_right (by simp) hne

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