LeanPool.DirectedTopologyLean4.DirectedSpace

class DirectedSpace (α : Type u) extends TopologicalSpace α : Type u

Definition of a directed topological space.

Dipaths are closed under:

• Constant paths,
• Concatenation of paths,
• Monotone reparametrization of paths.

• IsOpen : Set α → Prop
• isOpen_univ : TopologicalSpace.IsOpen Set.univ
• isOpen_inter (s t : Set α) : TopologicalSpace.IsOpen s → TopologicalSpace.IsOpen t → TopologicalSpace.IsOpen (s ∩ t)
• isOpen_sUnion (s : Set (Set α)) : (∀ t ∈ s, TopologicalSpace.IsOpen t) → TopologicalSpace.IsOpen (⋃₀ s)
• IsDipath {x y : α} : Path x y → Prop

  Predicate selecting the directed paths in the space.

• isDipath_constant (x : α) : IsDipath (Path.refl x)

  Every constant path is directed.

• isDipath_concat {x y z : α} {γ₁ : Path x y} {γ₂ : Path y z} : IsDipath γ₁ → IsDipath γ₂ → IsDipath (γ₁.trans γ₂)

  The concatenation of two directed paths is directed.

• isDipath_reparam {x y : α} {γ : Path x y} {t₀ t₁ : ↑unitInterval} {f : Path t₀ t₁} : Monotone ⇑f → IsDipath γ → IsDipath (f.map ⋯)

  Monotone reparametrization preserves directedness.

def IsDipath {α : Type u} {x y : α} [DirectedSpace α] : Path x y → Prop

A path in a directed space is a dipath if it satisfies the directed-space predicate.

Equations

• IsDipath = DirectedSpace.IsDipath

theorem isDipath_constant {α : Type u} [DirectedSpace α] (x : α) : IsDipath (Path.refl x)

The constant path at any point of a directed space is directed.

theorem isDipath_concat {α : Type u} {x y z : α} [DirectedSpace α] {γ : Path x y} {γ' : Path y z} (hγ : IsDipath γ) (hγ' : IsDipath γ') : IsDipath (γ.trans γ')

The concatenation of two dipaths is again a dipath.

theorem isDipath_reparam {α : Type u} {x y : α} [DirectedSpace α] {γ : Path x y} {t₀ t₁ : ↑unitInterval} {f : Path t₀ t₁} (hfmono : Monotone ⇑f) (hγ : IsDipath γ) : IsDipath (f.map ⋯)

Reparametrizing a dipath along a monotone path yields another dipath.

theorem isDipath_cast {α : Type u} [DirectedSpace α] {x y x' y' : α} (γ : Path x y) (hx : x' = x) (hy : y' = y) (hγ : IsDipath γ) : IsDipath (γ.cast hx hy)

Casting a path that is directed into another path gives another directed path