bind

Mathlib.MeasureTheory.Function.SimpleFunc

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

Lean4

/-- If `f : α →ₛ β` is a simple function and `g : β → α →ₛ γ` is a family of simple functions,
then `f.bind g` binds the first argument of `g` to `f`. In other words, `f.bind g a = g (f a) a`. -/
def bind (f : α →ₛ β) (g : β → α →ₛ γ) : α →ₛ γ :=
  ⟨fun a => g (f a) a, fun c => f.measurableSet_cut (fun a b => g b a = c) fun b => (g b).measurableSet_preimage { c },
    (f.finite_range.biUnion fun b _ => (g b).finite_range).subset <| by rintro _ ⟨a, rfl⟩; simp⟩

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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