fundamentalInterior_union_fundamentalFrontier

English

The fundamental interior together with the frontier recovers the original domain: fundamentalInterior(G,s) ∪ fundamentalFrontier(G,s) = s.

Русский

Внутренняя часть фундаментальной области вместе с границей восстанавливают исходную область: fundamentalInterior(G,s) ∪ fundamentalFrontier(G,s) = s.

LaTeX

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

Lean4

@[to_additive (attr := simp) MeasureTheory.addFundamentalInterior_union_addFundamentalFrontier]
theorem fundamentalInterior_union_fundamentalFrontier : fundamentalInterior G s ∪ fundamentalFrontier G s = s :=
  diff_union_inter _ _

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