self_diff_frontier

Mathlib.Topology.Closure

URI: https://scilib.ai/kg/mathlib#self_diff_frontier

← MathLib Explorer

English

A set minus its frontier equals its interior.

Русский

Множество минус своей границы равняется егоInterior.

LaTeX

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

Lean4

@[simp]
theorem self_diff_frontier (s : Set X) : s \ frontier s = interior s := by
  rw [frontier, diff_diff_right, diff_eq_empty.2 subset_closure, inter_eq_self_of_subset_right interior_subset,
    empty_union]

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

Научная платформа российской исследовательской школы.

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru