of_boundary_eq_empty

Mathlib.Geometry.Manifold.IsManifold.InteriorBoundary

URI: https://scilib.ai/kg/mathlib#ModelWithCorners.Boundaryless.of_boundary_eq_empty

← MathLib Explorer

English

M is boundaryless iff its boundary is empty.

Русский

M граница без границы тогда и только тогда, когда граница пустая.

LaTeX

$$$$ I.boundary M = \emptyset \iff BoundarylessManifold I M $$$$

Lean4

/-- Manifolds with empty boundary are boundaryless. -/
theorem of_boundary_eq_empty (h : I.boundary M = ∅) : BoundarylessManifold I M :=
  (Boundaryless.iff_boundary_eq_empty (I := I)).mp h

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

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

Разделы

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

Аффилиация

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