coborder_eq_compl_frontier_iff — Mathlib

English

Coborder equals the complement of the frontier if and only if s is open.

Русский

Coborder совпадает с комплементом предела границы тогда и только тогда, когда s открыто.

LaTeX

$$$\operatorname{coborder}(s) = (\operatorname{frontier}(s))^{c} \iff \text{IsOpen}(s)$$

Lean4

theorem coborder_eq_compl_frontier_iff : coborder s = (frontier s)ᶜ ↔ IsOpen s := by
  simp_rw [coborder_eq_union_frontier_compl, union_eq_right, subset_compl_iff_disjoint_left,
    disjoint_frontier_iff_isOpen]

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