Documentation

Mathlib.MeasureTheory.MeasurableSpace.PreorderRestrict

Measurability of the restriction function for functions indexed by a preorder #

We prove that the map which restricts a function f : (i : α) → X i to elements ≤ a is measurable.

theorem Preorder.measurable_restrictLe {α : Type u_1} [Preorder α] {X : αType u_2} [(a : α) → MeasurableSpace (X a)] (a : α) :
theorem Preorder.measurable_restrictLe₂ {α : Type u_1} [Preorder α] {X : αType u_2} [(a : α) → MeasurableSpace (X a)] {a : α} {b : α} (hab : a b) :
theorem Preorder.measurable_frestrictLe {α : Type u_1} [Preorder α] {X : αType u_2} [(a : α) → MeasurableSpace (X a)] [LocallyFiniteOrderBot α] (a : α) :
theorem Preorder.measurable_frestrictLe₂ {α : Type u_1} [Preorder α] {X : αType u_2} [(a : α) → MeasurableSpace (X a)] [LocallyFiniteOrderBot α] {a : α} {b : α} (hab : a b) :