instFintypeI₀FiniteSubcover

Mathlib.AlgebraicGeometry.Cover.Open

URI: https://scilib.ai/kg/mathlib#AlgebraicGeometry.Scheme.instFintypeI₀FiniteSubcover

English

If X is a compact space, the index set I₀ of a finite open cover is finite.

Русский

Если X компактное, индексный набор I₀ конечного открытого покрытия конечен.

LaTeX

$$$$ \text{Fintype}(\mathcal{U}.finiteSubcover.I_0) $$$$

Lean4

instance [H : CompactSpace X] : Fintype 𝒰.finiteSubcover.I₀ := by delta OpenCover.finiteSubcover; infer_instance

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

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

Разделы

Аффилиация

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