closure_diff_intrinsicFrontier — Mathlib

English

The closure of s minus its intrinsicFrontier equals the intrinsicInterior of s.

Русский

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

LaTeX

$$closure(s) \\ intrinsicFrontier_{\\mathbb{k}}(s) = intrinsicInterior_{\\mathbb{k}}(s)$$

Lean4

@[simp]
theorem closure_diff_intrinsicFrontier (s : Set P) : closure s \ intrinsicFrontier 𝕜 s = intrinsicInterior 𝕜 s :=
  intrinsicClosure_eq_closure 𝕜 s ▸ intrinsicClosure_diff_intrinsicFrontier s

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