fintype

Mathlib.Geometry.Manifold.PartitionOfUnity

URI: https://scilib.ai/kg/mathlib#SmoothBumpCovering.fintype

← MathLib Explorer

English

For each x, the set {i | fs i x ≠ 0} is finite.

Русский

Для каждого x множество {i | fs_i(x) ≠ 0} конечное.

LaTeX

$${ i | fs_i(x) ≠ 0 } is finite.$$

Lean4

/-- The index type of a `SmoothBumpCovering` of a compact manifold is finite. -/
protected def fintype [CompactSpace M] : Fintype ι :=
  fs.locallyFinite.fintypeOfCompact fun i => (fs i).nonempty_support

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

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

Разделы

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

Аффилиация

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