frontier_compl

Mathlib.Topology.Closure

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

← MathLib Explorer

English

The frontier of a set equals the frontier of its complement.

Русский

Граница множества равна границе его дополнения.

LaTeX

$$$frontier(s^c) = frontier(s)$$$

Lean4

/-- The complement of a set has the same frontier as the original set. -/
@[simp]
theorem frontier_compl (s : Set X) : frontier sᶜ = frontier s := by
  simp only [frontier_eq_closure_inter_closure, compl_compl, inter_comm]

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

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

Разделы

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

Аффилиация

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