IsTotallySeparated — Mathlib

English

The empty set is totally separated.

Русский

Пустое множество является полностью отделимым.

LaTeX

$$IsTotallySeparated (∅)$$

Lean4

/-- A set `s` is called totally separated if any two points of this set can be separated
by two disjoint open sets covering `s`. -/
def IsTotallySeparated (s : Set α) : Prop :=
  Set.Pairwise s fun x y => ∃ u v : Set α, IsOpen u ∧ IsOpen v ∧ x ∈ u ∧ y ∈ v ∧ s ⊆ u ∪ v ∧ Disjoint u v

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