intrinsicClosure_diff_intrinsicFrontier

English

The intrinsic closure minus the intrinsic frontier equals the intrinsic interior.

Русский

Разность внутреннего замыкания и внутренней границы равна внутренности.

LaTeX

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

Lean4

@[simp]
theorem intrinsicClosure_diff_intrinsicFrontier (s : Set P) :
    intrinsicClosure 𝕜 s \ intrinsicFrontier 𝕜 s = intrinsicInterior 𝕜 s :=
  (image_diff Subtype.coe_injective _ _).symm.trans <| by rw [closure_diff_frontier, intrinsicInterior]

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