eq_univ — Mathlib

English

For a Preconnected space, if a set s is clopen and nonempty, then s must be the whole space.

Русский

В предпредсвязанном пространстве, если множество клозоплосно и непусто, то оно совпадает с всем пространством.

LaTeX

$$$[PreconnectedSpace\;\alpha]\;IsClopen(s) \land s \neq \emptyset \Rightarrow s = \mathrm{univ}$$$

Lean4

theorem eq_univ [PreconnectedSpace α] {s : Set α} (h' : IsClopen s) (h : s.Nonempty) : s = univ :=
  (isClopen_iff.mp h').resolve_left h.ne_empty

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