IsBoundaryPoint — Mathlib

English

A point x ∈ M is a boundary point if and only if its image under the extended chart extChartAt I x x lies on the boundary of the model space, i.e., on the frontier of range I.

Русский

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

LaTeX

$$$$ I.IsBoundaryPoint(x) \iff extChartAt I x x \in frontier (range I) $$$$

Lean4

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

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