fundamentalFrontier_union_fundamentalInterior

English

The union of the frontier and the interior also covers the domain: frontier(G,s) ∪ interior(G,s) = s.

Русский

Объединение границы и внутренней части также покрывает домен: frontier(G,s) ∪ interior(G,s) = s.

LaTeX

$$$\\mathrm{fundamentalFrontier}(G,s) \\cup \\mathrm{fundamentalInterior}(G,s) = s$$$

Lean4

@[to_additive (attr := simp) MeasureTheory.addFundamentalFrontier_union_addFundamentalInterior]
theorem fundamentalFrontier_union_fundamentalInterior : fundamentalFrontier G s ∪ fundamentalInterior G s = s :=
  inter_union_diff _ _

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