# Continuous open maps #

This file defines bundled continuous open maps.

We use the DFunLike design, so each type of morphisms has a companion typeclass which is meant to be satisfied by itself and all stricter types.

## Types of morphisms #

• ContinuousOpenMap: Continuous open maps.

## Typeclasses #

• ContinuousOpenMapClass
structure ContinuousOpenMap (α : Type u_6) (β : Type u_7) [] [] extends :
Type (max u_6 u_7)

The type of continuous open maps from α to β, aka Priestley homomorphisms.

Instances For
theorem ContinuousOpenMap.map_open' {α : Type u_6} {β : Type u_7} [] [] (self : α →CO β) :
IsOpenMap self.toFun
Equations
Instances For
class ContinuousOpenMapClass (F : Type u_6) (α : outParam (Type u_7)) (β : outParam (Type u_8)) [] [] [FunLike F α β] extends :

ContinuousOpenMapClass F α β states that F is a type of continuous open maps.

You should extend this class when you extend ContinuousOpenMap.

• map_continuous : ∀ (f : F),
• map_open : ∀ (f : F),
Instances
theorem ContinuousOpenMapClass.map_open {F : Type u_6} {α : outParam (Type u_7)} {β : outParam (Type u_8)} [] [] [FunLike F α β] [self : ] (f : F) :
instance instCoeTCContinuousOpenMapOfContinuousOpenMapClass {F : Type u_1} {α : Type u_2} {β : Type u_3} [] [] [FunLike F α β] [] :
CoeTC F (α →CO β)
Equations
• instCoeTCContinuousOpenMapOfContinuousOpenMapClass = { coe := fun (f : F) => { toContinuousMap := f, map_open' := } }

### Continuous open maps #

instance ContinuousOpenMap.instFunLike {α : Type u_2} {β : Type u_3} [] [] :
FunLike (α →CO β) α β
Equations
• ContinuousOpenMap.instFunLike = { coe := fun (f : α →CO β) => f.toFun, coe_injective' := }
instance ContinuousOpenMap.instContinuousOpenMapClass {α : Type u_2} {β : Type u_3} [] [] :
Equations
• =
theorem ContinuousOpenMap.toFun_eq_coe {α : Type u_2} {β : Type u_3} [] [] {f : α →CO β} :
f.toFun = f
@[simp]
theorem ContinuousOpenMap.coe_toContinuousMap {α : Type u_2} {β : Type u_3} [] [] (f : α →CO β) :
f.toContinuousMap = f
theorem ContinuousOpenMap.ext {α : Type u_2} {β : Type u_3} [] [] {f : α →CO β} {g : α →CO β} (h : ∀ (a : α), f a = g a) :
f = g
def ContinuousOpenMap.copy {α : Type u_2} {β : Type u_3} [] [] (f : α →CO β) (f' : αβ) (h : f' = f) :
α →CO β

Copy of a ContinuousOpenMap with a new ContinuousMap equal to the old one. Useful to fix definitional equalities.

Equations
• f.copy f' h = { toContinuousMap := f.copy f' h, map_open' := }
Instances For
@[simp]
theorem ContinuousOpenMap.coe_copy {α : Type u_2} {β : Type u_3} [] [] (f : α →CO β) (f' : αβ) (h : f' = f) :
(f.copy f' h) = f'
theorem ContinuousOpenMap.copy_eq {α : Type u_2} {β : Type u_3} [] [] (f : α →CO β) (f' : αβ) (h : f' = f) :
f.copy f' h = f
def ContinuousOpenMap.id (α : Type u_2) [] :
α →CO α

id as a ContinuousOpenMap.

Equations
• = { toContinuousMap := , map_open' := }
Instances For
instance ContinuousOpenMap.instInhabited (α : Type u_2) [] :
Equations
• = { default := }
@[simp]
theorem ContinuousOpenMap.coe_id (α : Type u_2) [] :
= id
@[simp]
theorem ContinuousOpenMap.id_apply {α : Type u_2} [] (a : α) :
a = a
def ContinuousOpenMap.comp {α : Type u_2} {β : Type u_3} {γ : Type u_4} [] [] [] (f : β →CO γ) (g : α →CO β) :
α →CO γ

Composition of ContinuousOpenMaps as a ContinuousOpenMap.

Equations
• f.comp g = { toContinuousMap := f.comp g.toContinuousMap, map_open' := }
Instances For
@[simp]
theorem ContinuousOpenMap.coe_comp {α : Type u_2} {β : Type u_3} {γ : Type u_4} [] [] [] (f : β →CO γ) (g : α →CO β) :
(f.comp g) = f g
@[simp]
theorem ContinuousOpenMap.comp_apply {α : Type u_2} {β : Type u_3} {γ : Type u_4} [] [] [] (f : β →CO γ) (g : α →CO β) (a : α) :
(f.comp g) a = f (g a)
@[simp]
theorem ContinuousOpenMap.comp_assoc {α : Type u_2} {β : Type u_3} {γ : Type u_4} {δ : Type u_5} [] [] [] [] (f : γ →CO δ) (g : β →CO γ) (h : α →CO β) :
(f.comp g).comp h = f.comp (g.comp h)
@[simp]
theorem ContinuousOpenMap.comp_id {α : Type u_2} {β : Type u_3} [] [] (f : α →CO β) :
f.comp = f
@[simp]
theorem ContinuousOpenMap.id_comp {α : Type u_2} {β : Type u_3} [] [] (f : α →CO β) :
.comp f = f
@[simp]
theorem ContinuousOpenMap.cancel_right {α : Type u_2} {β : Type u_3} {γ : Type u_4} [] [] [] {g₁ : β →CO γ} {g₂ : β →CO γ} {f : α →CO β} (hf : ) :
g₁.comp f = g₂.comp f g₁ = g₂
@[simp]
theorem ContinuousOpenMap.cancel_left {α : Type u_2} {β : Type u_3} {γ : Type u_4} [] [] [] {g : β →CO γ} {f₁ : α →CO β} {f₂ : α →CO β} (hg : ) :
g.comp f₁ = g.comp f₂ f₁ = f₂