# Documentation

Mathlib.Topology.Hom.Open

# Continuous open maps #

This file defines bundled continuous open maps.

We use the FunLike 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
Instances For
class ContinuousOpenMapClass (F : Type u_6) (α : outParam (Type u_7)) (β : outParam (Type u_8)) [] [] extends :
Type (max (max u_6 u_7) u_8)
• coe : Fαβ
• coe_injective' : Function.Injective FunLike.coe
• map_continuous : ∀ (f : F),
• map_open : ∀ (f : F),

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

You should extend this class when you extend ContinuousOpenMap.

Instances
instance instCoeTCContinuousOpenMap {F : Type u_1} {α : Type u_2} {β : Type u_3} [] [] [] :
CoeTC F (α →CO β)

### Continuous open maps #

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.

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

id as a ContinuousOpenMap.

Instances For
@[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.

Instances For
@[simp]
theorem ContinuousOpenMap.coe_comp {α : Type u_2} {β : Type u_3} {γ : Type u_4} [] [] [] (f : β →CO γ) (g : α →CO β) :
↑() = f g
@[simp]
theorem ContinuousOpenMap.comp_apply {α : Type u_2} {β : Type u_3} {γ : Type u_4} [] [] [] (f : β →CO γ) (g : α →CO β) (a : α) :
↑() 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 β) :
@[simp]
theorem ContinuousOpenMap.comp_id {α : Type u_2} {β : Type u_3} [] [] (f : α →CO β) :
@[simp]
theorem ContinuousOpenMap.id_comp {α : Type u_2} {β : Type u_3} [] [] (f : α →CO β) :
@[simp]
theorem ContinuousOpenMap.cancel_right {α : Type u_2} {β : Type u_3} {γ : Type u_4} [] [] [] {g₁ : β →CO γ} {g₂ : β →CO γ} {f : α →CO β} (hf : ) :
g₁ = g₂
@[simp]
theorem ContinuousOpenMap.cancel_left {α : Type u_2} {β : Type u_3} {γ : Type u_4} [] [] [] {g : β →CO γ} {f₁ : α →CO β} {f₂ : α →CO β} (hg : ) :
f₁ = f₂