frontier_closure_subset

Mathlib.Topology.Closure

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

English

Frontier of closure is contained in frontier of the original set.

Русский

Граница замыкания множества ⊆ граница множества.

LaTeX

$$$frontier(closure(s)) \subseteq frontier(s)$$$

Lean4

theorem frontier_closure_subset : frontier (closure s) ⊆ frontier s :=
  diff_subset_diff closure_closure.subset <| interior_mono subset_closure

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

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

Разделы

Аффилиация

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