Continuity 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 continuous.

theorem Preorder.continuous_restrictLe {α : Type u_1} [Preorder α] {X : α → Type u_2} [(i : α) → TopologicalSpace (X i)] (a : α) : Continuous (Preorder.restrictLe a)

theorem Preorder.continuous_restrictLe₂ {α : Type u_1} [Preorder α] {X : α → Type u_2} [(i : α) → TopologicalSpace (X i)] {a b : α} (hab : a ≤ b) : Continuous (Preorder.restrictLe₂ hab)

theorem Preorder.continuous_frestrictLe {α : Type u_1} [Preorder α] {X : α → Type u_2} [(i : α) → TopologicalSpace (X i)] [LocallyFiniteOrderBot α] (a : α) : Continuous (Preorder.frestrictLe a)

theorem Preorder.continuous_frestrictLe₂ {α : Type u_1} [Preorder α] {X : α → Type u_2} [(i : α) → TopologicalSpace (X i)] [LocallyFiniteOrderBot α] {a b : α} (hab : a ≤ b) : Continuous (Preorder.frestrictLe₂ hab)