isInteriorPoint — Mathlib

English

The boundary is the complement of the interior and vice versa, as stated earlier.

Русский

Граница является дополнением внутренности и наоборот, как уже сказано ранее.

LaTeX

$$$$ I.boundary M = (I.interior M)^c \quad\text{and}\quad I.interior M = (I.boundary M)^c $$$$

Lean4

theorem _root_.BoundarylessManifold.isInteriorPoint {x : M} [BoundarylessManifold I M] : IsInteriorPoint I x :=
  BoundarylessManifold.isInteriorPoint' x

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