one_def

Mathlib.MeasureTheory.Function.AEEqFun

URI: https://scilib.ai/kg/mathlib#MeasureTheory.AEEqFun.one_def

English

The element 1 in the ae-equivalence world corresponds to the function constantly equal to 1.

Русский

Элемент 1 в ae-мире соответствует константной функции, принимающей значение 1.

LaTeX

$$$1 = mk (\lambda x. 1) aestronglyMeasurable_const$$$

Lean4

@[to_additive]
theorem one_def [One β] : (1 : α →ₘ[μ] β) = mk (fun _ : α => 1) aestronglyMeasurable_const :=
  rfl

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

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

Разделы

Аффилиация

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