disjoint_or_subset_of_isClopen — Mathlib

English

A preconnected set is either disjoint from a clopen set, or is contained in that clopen set.

Русский

Предсвязанное множество либо дизъюнктивно относительно клозного множества, либо содержится в нём.

LaTeX

$$$Disjoint s t \lor s \subseteq t$$$

Lean4

/-- Preconnected sets are either contained in or disjoint to any given clopen set. -/
theorem disjoint_or_subset_of_isClopen {s t : Set α} (hs : IsPreconnected s) (ht : IsClopen t) : Disjoint s t ∨ s ⊆ t :=
  (disjoint_or_nonempty_inter s t).imp_right <| hs.subset_isClopen ht

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