boundary_eq_empty

Mathlib.Geometry.Manifold.IsManifold.InteriorBoundary

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

← MathLib Explorer

English

Manifolds with boundaryless property imply the boundary is empty.

Русский

У многообразий без границы граница пустая.

LaTeX

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

Lean4

/-- Boundaryless manifolds have empty boundary. -/
theorem boundary_eq_empty [BoundarylessManifold I M] : I.boundary M = ∅ := by
  rw [← I.compl_interior, I.interior_eq_univ, compl_empty_iff]

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

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

Разделы

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

Аффилиация

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