instIsEmptyElemBoundaryOfBoundarylessManifold

Mathlib.Geometry.Manifold.IsManifold.InteriorBoundary

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

English

There exists an instance making a boundaryless manifold when certain conditions hold.

Русский

Существует пример, задающий границу как пустую при выполнении условий.

LaTeX

$$$$ \text{Instance: } BoundarylessManifold I M $$$$

Lean4

instance [BoundarylessManifold I M] : IsEmpty (I.boundary M) :=
  isEmpty_coe_sort.mpr Boundaryless.boundary_eq_empty

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

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

Разделы

Аффилиация

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