frontier_eq_inter_compl_interior — Mathlib

English

The frontier equals the intersection of the complement of the interior with the complement of the interior of the complement: frontier(s) = (interior(s))^c ∩ (interior(s^c))^c.

Русский

Граница множества равна пересечению комплемента interior с комплементом interior от дополнения: frontier(s) = (interior(s))^c ∩ (interior(s^c))^c.

LaTeX

$$$\\operatorname{frontier}(s) = (\\operatorname{interior}(s))^c \\cap (\\operatorname{interior}(s^c))^c$$$

Lean4

theorem frontier_eq_inter_compl_interior : frontier s = (interior s)ᶜ ∩ (interior sᶜ)ᶜ := by
  rw [← frontier_compl, ← closure_compl, ← diff_eq, closure_diff_interior]

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