of_empty

Mathlib.Geometry.Manifold.IsManifold.InteriorBoundary

URI: https://scilib.ai/kg/mathlib#ModelWithCorners.BoundarylessManifold.of_empty

← MathLib Explorer

English

The boundary of the manifold M is defined as the set of its boundary points.

Русский

Граница многообразия M определяется как множество его граничных точек.

LaTeX

$$$$ \text{boundary} \ M = \{ x \in M \mid I.IsBoundaryPoint x \} $$$$

Lean4

/-- The empty manifold is boundaryless. -/
instance of_empty [IsEmpty M] : BoundarylessManifold I M where isInteriorPoint' x := (IsEmpty.false x).elim

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

Научная платформа российской исследовательской школы.

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru