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 : α) : Measurable (Preorder.restrictLe a)

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

theorem Preorder.measurable_frestrictLe {α : Type u_1} [Preorder α] {X : α → Type u_2} [(a : α) → MeasurableSpace (X a)] [LocallyFiniteOrderBot α] (a : α) : Measurable (Preorder.frestrictLe a)

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