intrinsicClosure_diff_intrinsicInterior

English

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

Русский

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

LaTeX

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

Lean4

@[simp]
theorem intrinsicClosure_diff_intrinsicInterior (s : Set P) :
    intrinsicClosure 𝕜 s \ intrinsicInterior 𝕜 s = intrinsicFrontier 𝕜 s :=
  (image_diff Subtype.coe_injective _ _).symm

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