interior — Mathlib

English

The interior of a manifold is the set of interior points, i.e., points where I.IsInteriorPoint holds.

Русский

Внутренняя часть многообразия — это множество внутренних точек, то есть точек, для которых выполняется I.IsInteriorPoint.

LaTeX

$$$$ \text{The interior is } I.interior\ M = \{ x \in M \mid I.IsInteriorPoint x \} $$$$

Lean4

/-- The **interior** of a manifold `M` is the set of its interior points. -/
protected def interior : Set M :=
  {x : M | I.IsInteriorPoint x}

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