instMeasurableSingletonClass

Mathlib.MeasureTheory.MeasurableSpace.Constructions

URI: https://scilib.ai/kg/mathlib#Set.instMeasurableSingletonClass

English

For a Countable α, the type Set α carries a MeasurableSingletonClass.

Русский

Для счётного множества α тип Set α обладает свойством MeasurableSingletonClass.

LaTeX

$$$[ \text{Countable } \alpha ] \Rightarrow \mathrm{MeasurableSingletonClass}(\mathrm{Set}(\alpha))$$$

Lean4

instance instMeasurableSingletonClass [Countable α] : MeasurableSingletonClass (Set α) := by unfold Set; infer_instance

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

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

Разделы

Аффилиация

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