disjoint_frontier_iff_isOpen — Mathlib

English

The frontier of s is disjoint from t if and only if t is open.

Русский

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

LaTeX

$$$\\operatorname{Disjoint}(\\operatorname{frontier}(s), t) \\iff \\operatorname{IsOpen}(s)$$$

Lean4

theorem disjoint_frontier_iff_isOpen : Disjoint (frontier s) s ↔ IsOpen s := by
  rw [← isClosed_compl_iff, ← frontier_subset_iff_isClosed, frontier_compl, subset_compl_iff_disjoint_right]

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