const

Mathlib.MeasureTheory.MeasurableSpace.Defs

URI: https://scilib.ai/kg/mathlib#MeasurableSet.const

English

For any proposition p, the set {a ∈ α | p} is measurable.

Русский

Для любого утверждения p множество {a ∈ α | p} измеримо.

LaTeX

$$$p \text{ is arbitrary} \Rightarrow \mathrm{MeasurableSet}({a:\alpha \mid p})$$$

Lean4

protected theorem const (p : Prop) : MeasurableSet {_a : α | p} := by by_cases p <;> simp [*]

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

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

Разделы

Аффилиация

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