subset_coborder — Mathlib

English

For any set s in a topological space X, we have s ⊆ coborder(s); the coborder always contains the set itself.

Русский

Для любого множества s в топологическом пространстве X выполняется s ⊆ coborder(s); coborder всегда содержит само множество.

LaTeX

$$$s \subseteq \operatorname{coborder}(s)$$$

Lean4

theorem subset_coborder : s ⊆ coborder s :=
  by
  rw [coborder, subset_compl_iff_disjoint_right]
  exact disjoint_sdiff_self_right

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