bind_const

Mathlib.MeasureTheory.Function.SimpleFunc

URI: https://scilib.ai/kg/mathlib#MeasureTheory.SimpleFunc.bind_const

English

For any simple function f: α →ₛ β, binding f with the constant function yields f again; i.e., f.bind(const α) = f.

Русский

Для любой простой функции f: α →ₛ β связывание f константной функцией даёт ту же функцию; то есть f.bind(const α) = f.

LaTeX

$$$f \bind (\text{const } α) = f$$$

Lean4

@[simp]
theorem bind_const (f : α →ₛ β) : f.bind (const α) = f := by ext; simp

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

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

Разделы

Аффилиация

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