LeanPool.DirectedTopologyLean4.DirectedMap

def DirectedMap.Directed {α : Type u_1} {β : Type u_2} [DirectedSpace α] [DirectedSpace β] (f : C(α, β)) : Prop

A continuous map between two directed spaces is Directed if it maps dipaths to dipaths.

Equations

• DirectedMap.Directed f = ∀ ⦃x y : α⦄ (γ : Path x y), IsDipath γ → IsDipath (γ.map ⋯)

structure DirectedMap (α : Type u_1) (β : Type u_2) [DirectedSpace α] [DirectedSpace β] extends C(α, β) : Type (max u_1 u_2)

Define the type of a directed map

• toFun : α → β
• continuous_toFun : Continuous self.toFun
• directed_toFun : Directed self.toContinuousMap

def «termD(_,_)» : Lean.ParserDescr

Notation D(X,Y) for directed maps from X to Y

Equations

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

class DirectedMapClass (F : Type u_1) (α : outParam (Type u_2)) (β : outParam (Type u_3)) [DirectedSpace α] [DirectedSpace β] [FunLike F α β] extends ContinuousMapClass F α β : Prop

Type class for the bundled directed maps from α to β.

• map_continuous (f : F) : Continuous ⇑f
• map_directed (f : F) : DirectedMap.Directed ↑f

  Each element of the class is directed when viewed as a continuous map.

def toDirectedMap {F : Type u_1} {α : Type u_2} {β : Type u_3} [DirectedSpace α] [DirectedSpace β] [FunLike F α β] [hF : DirectedMapClass F α β] (f : F) : D(α,β)

Coerce a member of a DirectedMapClass to the bundled directed map type D(α, β).

Equations

• ↑f = { toContinuousMap := ↑f, directed_toFun := ⋯ }

@[implicit_reducible]

instance instCoeTCDirectedMap {F : Type u_1} {α : Type u_2} {β : Type u_3} [DirectedSpace α] [DirectedSpace β] [FunLike F α β] [hF : DirectedMapClass F α β] : CoeTC F D(α,β)

Equations

• instCoeTCDirectedMap = { coe := toDirectedMap }

@[implicit_reducible]

instance DirectedMap.instFunLike {α : Type u_1} {β : Type u_2} [DirectedSpace α] [DirectedSpace β] : FunLike D(α,β) α β

Equations

• DirectedMap.instFunLike = { coe := fun (f : D(α,β)) => f.toFun, coe_injective := ⋯ }

instance DirectedMap.toDirectedMapClass {α : Type u_1} {β : Type u_2} [DirectedSpace α] [DirectedSpace β] : DirectedMapClass D(α,β) α β

@[implicit_reducible]

instance DirectedMap.instCoeFunForall {α : Type u_1} {β : Type u_2} [DirectedSpace α] [DirectedSpace β] : CoeFun D(α,β) fun (x : D(α,β)) => α → β

Helper instance for when there's too many metavariables to apply FunLike.hasCoeToFun directly.

Equations

• DirectedMap.instCoeFunForall = DFunLike.toCoeFun

@[implicit_reducible]

instance DirectedMap.instCoeContinuousMap {α : Type u_1} {β : Type u_2} [DirectedSpace α] [DirectedSpace β] : Coe D(α,β) C(α, β)

A directed map can be coerced into a continuous map

Equations

• DirectedMap.instCoeContinuousMap = { coe := fun (f : D(α,β)) => f.toContinuousMap }

@[simp]

theorem DirectedMap.toFun_eq_coe {α : Type u_1} {β : Type u_2} [DirectedSpace α] [DirectedSpace β] {f : D(α,β)} : f.toFun = ⇑f

@[simp]

theorem DirectedMap.coe_to_continuous_map {α : Type u_1} {β : Type u_2} [DirectedSpace α] [DirectedSpace β] (f : D(α,β)) : ⇑f.toContinuousMap = ⇑f

@[simp]

theorem DirectedMap.coe_coe {α : Type u_1} {β : Type u_2} [DirectedSpace α] [DirectedSpace β] {F : Type u_5} [FunLike F α β] [DirectedMapClass F α β] (f : F) : ⇑↑f = ⇑f

theorem DirectedMap.ext {α : Type u_1} {β : Type u_2} [DirectedSpace α] [DirectedSpace β] {f g : D(α,β)} (h : ∀ (x : α), f x = g x) : f = g

theorem DirectedMap.ext_iff {α : Type u_1} {β : Type u_2} [DirectedSpace α] [DirectedSpace β] {f g : D(α,β)} : f = g ↔ ∀ (x : α), f x = g x

def DirectedMap.id (α : Type u_1) [DirectedSpace α] : D(α,α)

The identity map is directed

Equations

• DirectedMap.id α = { toFun := id, continuous_toFun := ⋯, directed_toFun := ⋯ }

@[simp]

theorem DirectedMap.coe_id (α : Type u_1) [DirectedSpace α] : ⇑(DirectedMap.id α) = id

def DirectedMap.const (α : Type u_1) {β : Type u_2} [DirectedSpace α] [DirectedSpace β] (b : β) : D(α,β)

Constant maps are directed

Equations

• DirectedMap.const α b = { toFun := fun (x : α) => b, continuous_toFun := ⋯, directed_toFun := ⋯ }

@[simp]

theorem DirectedMap.coe_const (α : Type u_1) {β : Type u_2} [DirectedSpace α] [DirectedSpace β] (b : β) : ⇑(const α b) = Function.const α b

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

The composition of directed maps is directed

Equations

• f.comp g = { toFun := ⇑f ∘ ⇑g, continuous_toFun := ⋯, directed_toFun := ⋯ }

@[simp]

theorem DirectedMap.id_apply {α : Type u_1} [DirectedSpace α] (a : α) : (DirectedMap.id α) a = a

@[simp]

theorem DirectedMap.const_apply {α : Type u_1} {β : Type u_2} [DirectedSpace α] [DirectedSpace β] (b : β) (a : α) : (const α b) a = b

@[simp]

theorem DirectedMap.coe_comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} [DirectedSpace α] [DirectedSpace β] [DirectedSpace γ] (f : D(β,γ)) (g : D(α,β)) : ⇑(f.comp g) = ⇑f ∘ ⇑g

@[simp]

theorem DirectedMap.comp_apply {α : Type u_1} {β : Type u_2} {γ : Type u_3} [DirectedSpace α] [DirectedSpace β] [DirectedSpace γ] (f : D(β,γ)) (g : D(α,β)) (a : α) : (f.comp g) a = f (g a)

@[simp]

theorem DirectedMap.comp_assoc {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} [DirectedSpace α] [DirectedSpace β] [DirectedSpace γ] [DirectedSpace δ] (f : D(γ,δ)) (g : D(β,γ)) (h : D(α,β)) : (f.comp g).comp h = f.comp (g.comp h)

@[simp]

theorem DirectedMap.id_comp {α : Type u_1} {β : Type u_2} [DirectedSpace α] [DirectedSpace β] (f : D(α,β)) : (DirectedMap.id β).comp f = f

@[simp]

theorem DirectedMap.comp_id {α : Type u_1} {β : Type u_2} [DirectedSpace α] [DirectedSpace β] (f : D(α,β)) : f.comp (DirectedMap.id α) = f

@[simp]

theorem DirectedMap.const_comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} [DirectedSpace α] [DirectedSpace β] [DirectedSpace γ] (c : γ) (f : D(α,β)) : (const β c).comp f = const α c

@[simp]

theorem DirectedMap.comp_const {α : Type u_1} {β : Type u_2} {γ : Type u_3} [DirectedSpace α] [DirectedSpace β] [DirectedSpace γ] (f : D(β,γ)) (b : β) : f.comp (const α b) = const α (f b)

theorem DirectedMap.coe_injective {α : Type u_1} {β : Type u_2} [DirectedSpace α] [DirectedSpace β] : Function.Injective DFunLike.coe