measurable_ncard

Mathlib.MeasureTheory.MeasurableSpace.NCard

URI: https://scilib.ai/kg/mathlib#measurable_ncard

English

For countable α, the ncard map from sets to natural numbers is measurable.

Русский

Для счетного α отображение ncard: Set α → ℕ измеримо.

LaTeX

$$$\\mathrm{Measurable}(\\mathrm{Set.ncard} : \\mathrm{Set} \\alpha \\to \\mathbb{N})$$$

Lean4

@[measurability]
theorem measurable_ncard : Measurable (Set.ncard : Set α → ℕ) :=
  Measurable.of_discrete.comp measurable_encard

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

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

Разделы

Аффилиация

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