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)
: