LeanPool.DirectedTopologyLean4.MonotonePath

theorem monotone_path_bounded_left {α : Type u_1} {x y : α} [TopologicalSpace α] [Preorder α] {γ : Path x y} (hγ : Monotone ⇑γ) (t : ↑unitInterval) : x ≤ γ t

theorem monotone_path_bounded_right {α : Type u_1} {x y : α} [TopologicalSpace α] [Preorder α] {γ : Path x y} (hγ : Monotone ⇑γ) (t : ↑unitInterval) : γ t ≤ y

theorem monotone_path_bounded {α : Type u_1} {x y : α} [TopologicalSpace α] [Preorder α] {γ : Path x y} (hγ : Monotone ⇑γ) (t : ↑unitInterval) : x ≤ γ t ∧ γ t ≤ y

theorem monotone_path_source_le_target {α : Type u_1} {x y : α} [TopologicalSpace α] [Preorder α] {γ : Path x y} (hγ : Monotone ⇑γ) : x ≤ y