closure_diff_frontier — Mathlib

English

Closure of s minus its frontier equals interior s.

Русский

Замыкание множества минус его граница равно внутренности множества.

LaTeX

$$$\overline{s} \setminus \operatorname{frontier}(s) = \operatorname{interior}(s)$$$

Lean4

@[simp]
theorem closure_diff_frontier (s : Set X) : closure s \ frontier s = interior s := by
  rw [frontier, diff_diff_right_self, inter_eq_self_of_subset_right interior_subset_closure]

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