# 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.

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