compl_boundary

Mathlib.Geometry.Manifold.IsManifold.InteriorBoundary

URI: https://scilib.ai/kg/mathlib#ModelWithCorners.compl_boundary

← MathLib Explorer

English

The interior is the complement of the boundary: interior M = (boundary M)^c.

Русский

Внутренняя часть — дополнение границы: interior M = (boundary M)^c.

LaTeX

$$$$ I.interior M = (I.boundary M)^{c} $$$$

Lean4

/-- The interior is the complement of the boundary. -/
theorem compl_boundary : (I.boundary M)ᶜ = I.interior M := by rw [← compl_interior, compl_compl]

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

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

Разделы

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

Аффилиация

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