LeanPool.DirectedTopologyLean4.Constructions

@[reducible]

def DirectedSpace.Preorder (α : Type u) [TopologicalSpace α] [_root_.Preorder α] : DirectedSpace α

Any space with a preorder can be equiped with a directedness, by allowing all monotone paths as directed paths

Equations

• DirectedSpace.Preorder α = { toTopologicalSpace := inst✝¹, IsDipath := fun {x y : α} (γ : Path x y) => Monotone ⇑γ, isDipath_constant := ⋯, isDipath_concat := ⋯, isDipath_reparam := ⋯ }

@[reducible]

def DirectedSpace.Induced {α : Type u} {β : Type v} [TopologicalSpace α] [hβ : DirectedSpace β] {f : α → β} (hf : Continuous f) : DirectedSpace α

A continuous map f : α → β with α an (undirected) topological space and β a directed topological space creates a directed structure on α by pulling back paths.

Equations

• One or more equations did not get rendered due to their size.

@[instance_reducible]

instance DirectedSubspace {α : Type u} {p : α → Prop} [DirectedSpace α] : DirectedSpace (Subtype p)

Equations

• DirectedSubspace = DirectedSpace.Induced ⋯

theorem directed_induced {α : Type u} {β : Type v} [TopologicalSpace α] [hβ : DirectedSpace β] (f : C(α, β)) : DirectedMap.Directed f

def DirectedSubtypeInclusion {α : Type u} (p : α → Prop) [DirectedSpace α] : D(Subtype p,α)

The inclusion of a subtype with the induced directed structure into the ambient space is a directed map.

Equations

• DirectedSubtypeInclusion p = { toFun := fun (x : Subtype p) => ↑x, continuous_toFun := ⋯, directed_toFun := ⋯ }

def DirectedSubsetInclusion {α : Type u} [t : DirectedSpace α] {X Y : Set α} (h : X ⊆ Y) : D(↑X,↑Y)

The inclusion of one subset into another, when both carry the induced directed structure, is a directed map.

Equations

• DirectedSubsetInclusion h = { toFun := Set.inclusion h, continuous_toFun := ⋯, directed_toFun := ⋯ }

@[instance_reducible]

instance DirectedProduct {α : Type u} {β : Type v} [t₁ : DirectedSpace α] [t₂ : DirectedSpace β] : DirectedSpace (α × β)

Equations

• One or more equations did not get rendered due to their size.

def directedFst {α : Type u_1} {β : Type u_2} [DirectedSpace α] [DirectedSpace β] : D(α × β,α)

The projection map α × β → α

Equations

• directedFst = { toFun := fun (x : α × β) => x.1, continuous_toFun := ⋯, directed_toFun := ⋯ }

def directedSnd {α : Type u_1} {β : Type u_2} [DirectedSpace α] [DirectedSpace β] : D(α × β,β)

The projection map α × β → β

Equations

• directedSnd = { toFun := fun (x : α × β) => x.2, continuous_toFun := ⋯, directed_toFun := ⋯ }

def DirectedMap.prodMapMk {α : Type u_1} {β : Type u_2} {γ : Type u_3} [DirectedSpace α] [DirectedSpace β] [DirectedSpace γ] (f : D(α,β)) (g : D(α,γ)) : D(α,β × γ)

Two directed maps f : α → β and g : α → γ can be turned into a directed map α → β × γ by mapping a : α to (f a, g a).

Equations

• f.prodMapMk g = { toFun := fun (x : α) => (f x, g x), continuous_toFun := ⋯, directed_toFun := ⋯ }

def DirectedMap.prodMapMk' {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} [DirectedSpace α] [DirectedSpace β] [DirectedSpace γ] [DirectedSpace δ] (f : D(α,γ)) (g : D(β,δ)) : D(α × β,γ × δ)

Two directed maps f : α → γ and g : β → δ can be turned into a directed map α × β → β × γ by mapping (a, b) : α × β to (f a, g b).

Equations

• f.prodMapMk' g = { toFun := fun (x : α × β) => (f x.1, g x.2), continuous_toFun := ⋯, directed_toFun := ⋯ }

def DirectedMap.prodConstFst {α : Type u_1} {β : Type u_2} {γ : Type u_3} [DirectedSpace α] [DirectedSpace β] [DirectedSpace γ] (F : D(α × β,γ)) (a : α) : D(β,γ)

For every t : α, we can convert a directed map F : α × β → γ to a directed map β → γ by sending b to F(t, b)

Equations

• F.prodConstFst a = F.comp ((DirectedMap.const β a).prodMapMk (DirectedMap.id β))

@[simp]

theorem DirectedMap.prod_const_fst_apply {α : Type u_1} {β : Type u_2} {γ : Type u_3} [DirectedSpace α] [DirectedSpace β] [DirectedSpace γ] (F : D(α × β,γ)) (a : α) (b : β) : (F.prodConstFst a) b = F (a, b)

def DirectedMap.prodConstSnd {α : Type u_1} {β : Type u_2} {γ : Type u_3} [DirectedSpace α] [DirectedSpace β] [DirectedSpace γ] (F : D(α × β,γ)) (t : β) : D(α,γ)

For every t : β, we can convert a directed map F : α × β → γ to a directed map α → γ by sending a to F(a, t)

Equations

• F.prodConstSnd t = F.comp ((DirectedMap.id α).prodMapMk (DirectedMap.const α t))

@[simp]

theorem DirectedMap.prod_const_snd_apply {α : Type u_1} {β : Type u_2} {γ : Type u_3} [DirectedSpace α] [DirectedSpace β] [DirectedSpace γ] (F : D(α × β,γ)) (b : β) (a : α) : (F.prodConstSnd b) a = F (a, b)