frontier_eq_empty_iff — Mathlib

English

In a Preconnected space, the frontier of a subset is empty if and only if the subset is either empty or the whole space.

Русский

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

LaTeX

$$$[PreconnectedSpace\alpha] \; frontier(s) = \emptyset \iff (s = \emptyset \lor s = \text{univ})$$$

Lean4

theorem frontier_eq_empty_iff [PreconnectedSpace α] {s : Set α} : frontier s = ∅ ↔ s = ∅ ∨ s = univ :=
  isClopen_iff_frontier_eq_empty.symm.trans isClopen_iff

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