coeFn_one

Mathlib.MeasureTheory.Function.AEEqFun

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

English

The coeFn_one lemma asserts that the constant-one ae-class is the cast of 1 by the evaluation map.

Русский

Лемма coeFn_one утверждает, что ae-класс единицы является отображением 1 через отображение cast.

LaTeX

$$$\text{coeFn_one}: (1 : α →_μ β) = 1$, up to ae-equivalence.$$

Lean4

@[to_additive]
theorem coeFn_one [One β] : ⇑(1 : α →ₘ[μ] β) =ᵐ[μ] 1 :=
  coeFn_const ..

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

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

Разделы

Аффилиация

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