intrinsicInterior_union_intrinsicFrontier

English

The intrinsic interior and intrinsic frontier together form the intrinsic closure.

Русский

Внутренняя часть и внутренняя граница вместе образуют внутреннее замыкание.

LaTeX

$$$\\operatorname{intrinsicInterior}_{\\mathbb{k}}(s) \\cup \\operatorname{intrinsicFrontier}_{\\mathbb{k}}(s) = \\operatorname{intrinsicClosure}_{\\mathbb{k}}(s)$$$

Lean4

@[simp]
theorem intrinsicInterior_union_intrinsicFrontier (s : Set P) :
    intrinsicInterior 𝕜 s ∪ intrinsicFrontier 𝕜 s = intrinsicClosure 𝕜 s := by
  simp [intrinsicClosure, intrinsicInterior, intrinsicFrontier, closure_eq_interior_union_frontier, image_union]

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