IsInteriorPoint — Mathlib

English

Let x be a point in the manifold M. Then x is interior iff its image under the extended chart extChartAt I x x lies in the interior of the model space range.

Русский

Пусть x — точка многообразия M. Тогда x является внутренней тогда и только тогда, когда её образ под расширенной картой extChartAt I x x лежит во внутренности моделируемого пространства range.

LaTeX

$$$$ I.IsInteriorPoint(x) \iff extChartAt I x x \in interior (range I) $$$$

Lean4

/-- `p ∈ M` is an interior point of a manifold `M` iff its image in the extended chart
lies in the interior of the model space. -/
def IsInteriorPoint (x : M) :=
  extChartAt I x x ∈ interior (range I)

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