index_countable

Mathlib.MeasureTheory.Covering.VitaliFamily

URI: https://scilib.ai/kg/mathlib#VitaliFamily.FineSubfamilyOn.index_countable

← MathLib Explorer

English

If the ambient space X is second countable, then h.index is a countable set.

Русский

Если пространство X второй счетно, то h.index счетно.

LaTeX

$$$[SecondCountableTopology\\ X]\\Rightarrow h.index\\text{ is countable}.$$$

Lean4

theorem index_countable [SecondCountableTopology X] : h.index.Countable :=
  h.covering_disjoint.countable_of_nonempty_interior fun _ hx => v.nonempty_interior _ _ (h.covering_mem_family hx)

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

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

Разделы

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

Аффилиация

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