closure_diff_intrinsicInterior — Mathlib

English

The intrinsic closure commutes with affine isometries: the image of intrinsicClosure under φ equals the intrinsicClosure of the image.

Русский

Образ внутреннего замыкания при аффинной изометрии совпадает с внутренним замыканием образа.

LaTeX

$$intrinsicClosure_{\\mathbb{k}}(φ''s) = φ'' intrinsicClosure_{\\mathbb{k}}(s)$$

Lean4

@[simp]
theorem closure_diff_intrinsicInterior (s : Set P) : closure s \ intrinsicInterior 𝕜 s = intrinsicFrontier 𝕜 s :=
  intrinsicClosure_eq_closure 𝕜 s ▸ intrinsicClosure_diff_intrinsicInterior s

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