# Continuous bundled maps #

In this file we define the type ContinuousMap of continuous bundled 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.

structure ContinuousMap (α : Type u_1) (β : Type u_2) [] [] :
Type (max u_1 u_2)

The type of continuous maps from α to β.

When possible, instead of parametrizing results over (f : C(α, β)), you should parametrize over {F : Type*} [ContinuousMapClass F α β] (f : F).

When you extend this structure, make sure to extend ContinuousMapClass.

• toFun : αβ

The function α → β

• continuous_toFun : Continuous self.toFun

Proposition that toFun is continuous

Instances For
theorem ContinuousMap.continuous_toFun {α : Type u_1} {β : Type u_2} [] [] (self : C(α, β)) :
Continuous self.toFun

Proposition that toFun is continuous

The type of continuous maps from α to β.

Equations
• One or more equations did not get rendered due to their size.
Instances For
class ContinuousMapClass (F : Type u_1) (α : Type u_2) (β : Type u_3) [] [] [FunLike F α β] :

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

You should extend this class when you extend ContinuousMap.

• map_continuous : ∀ (f : F),

Continuity

Instances
theorem ContinuousMapClass.map_continuous {F : Type u_1} {α : Type u_2} {β : Type u_3} [] [] [FunLike F α β] [self : ] (f : F) :

Continuity

theorem map_continuousAt {F : Type u_1} {α : Type u_2} {β : Type u_3} [] [] [FunLike F α β] [] (f : F) (a : α) :
ContinuousAt (⇑f) a
theorem map_continuousWithinAt {F : Type u_1} {α : Type u_2} {β : Type u_3} [] [] [FunLike F α β] [] (f : F) (s : Set α) (a : α) :
def toContinuousMap {F : Type u_1} {α : Type u_2} {β : Type u_3} [] [] [FunLike F α β] [] (f : F) :
C(α, β)

Coerce a bundled morphism with a ContinuousMapClass instance to a ContinuousMap.

Equations
• f = { toFun := f, continuous_toFun := }
Instances For
instance instCoeTCContinuousMap {F : Type u_1} {α : Type u_2} {β : Type u_3} [] [] [FunLike F α β] [] :
CoeTC F C(α, β)
Equations
• instCoeTCContinuousMap = { coe := toContinuousMap }

### Continuous maps #

instance ContinuousMap.funLike {α : Type u_1} {β : Type u_2} [] [] :
FunLike C(α, β) α β
Equations
• ContinuousMap.funLike = { coe := ContinuousMap.toFun, coe_injective' := }
instance ContinuousMap.toContinuousMapClass {α : Type u_1} {β : Type u_2} [] [] :
Equations
• =
@[simp]
theorem ContinuousMap.toFun_eq_coe {α : Type u_1} {β : Type u_2} [] [] {f : C(α, β)} :
f.toFun = f
instance ContinuousMap.instCanLiftForallCoeContinuous {α : Type u_1} {β : Type u_2} [] [] :
CanLift (αβ) C(α, β) DFunLike.coe Continuous
Equations
• =
def ContinuousMap.Simps.apply {α : Type u_1} {β : Type u_2} [] [] (f : C(α, β)) :
αβ

See note [custom simps projection].

Equations
Instances For
@[simp]
theorem ContinuousMap.coe_coe {α : Type u_1} {β : Type u_2} [] [] {F : Type u_5} [FunLike F α β] [] (f : F) :
f = f
theorem ContinuousMap.ext_iff {α : Type u_1} {β : Type u_2} [] [] {f : C(α, β)} {g : C(α, β)} :
f = g ∀ (a : α), f a = g a
theorem ContinuousMap.ext {α : Type u_1} {β : Type u_2} [] [] {f : C(α, β)} {g : C(α, β)} (h : ∀ (a : α), f a = g a) :
f = g
def ContinuousMap.copy {α : Type u_1} {β : Type u_2} [] [] (f : C(α, β)) (f' : αβ) (h : f' = f) :
C(α, β)

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

Equations
• f.copy f' h = { toFun := f', continuous_toFun := }
Instances For
@[simp]
theorem ContinuousMap.coe_copy {α : Type u_1} {β : Type u_2} [] [] (f : C(α, β)) (f' : αβ) (h : f' = f) :
(f.copy f' h) = f'
theorem ContinuousMap.copy_eq {α : Type u_1} {β : Type u_2} [] [] (f : C(α, β)) (f' : αβ) (h : f' = f) :
f.copy f' h = f
theorem ContinuousMap.continuous {α : Type u_1} {β : Type u_2} [] [] (f : C(α, β)) :

Deprecated. Use map_continuous instead.

theorem ContinuousMap.continuous_set_coe {α : Type u_1} {β : Type u_2} [] [] (s : Set C(α, β)) (f : s) :
Continuous f
theorem ContinuousMap.continuousAt {α : Type u_1} {β : Type u_2} [] [] (f : C(α, β)) (x : α) :
ContinuousAt (⇑f) x

Deprecated. Use map_continuousAt instead.

theorem ContinuousMap.congr_fun {α : Type u_1} {β : Type u_2} [] [] {f : C(α, β)} {g : C(α, β)} (H : f = g) (x : α) :
f x = g x

Deprecated. Use DFunLike.congr_fun instead.

theorem ContinuousMap.congr_arg {α : Type u_1} {β : Type u_2} [] [] (f : C(α, β)) {x : α} {y : α} (h : x = y) :
f x = f y

Deprecated. Use DFunLike.congr_arg instead.

theorem ContinuousMap.coe_injective {α : Type u_1} {β : Type u_2} [] [] :
Function.Injective DFunLike.coe
@[simp]
theorem ContinuousMap.coe_mk {α : Type u_1} {β : Type u_2} [] [] (f : αβ) (h : ) :
{ toFun := f, continuous_toFun := h } = f
theorem ContinuousMap.map_specializes {α : Type u_1} {β : Type u_2} [] [] (f : C(α, β)) {x : α} {y : α} (h : x y) :
f x f y
@[simp]
theorem ContinuousMap.equivFnOfDiscrete_symm_apply_apply (α : Type u_1) (β : Type u_2) [] [] [] (f : αβ) :
∀ (a : α), (.symm f) a = f a
@[simp]
theorem ContinuousMap.equivFnOfDiscrete_apply (α : Type u_1) (β : Type u_2) [] [] [] (f : C(α, β)) (a : α) :
f a = f a
def ContinuousMap.equivFnOfDiscrete (α : Type u_1) (β : Type u_2) [] [] [] :
C(α, β) (αβ)

The continuous functions from α to β are the same as the plain functions when α is discrete.

Equations
• = { toFun := fun (f : C(α, β)) => f, invFun := fun (f : αβ) => { toFun := f, continuous_toFun := }, left_inv := , right_inv := }
Instances For
def ContinuousMap.id (α : Type u_1) [] :
C(α, α)

The identity as a continuous map.

Equations
• = { toFun := id, continuous_toFun := }
Instances For
@[simp]
theorem ContinuousMap.coe_id (α : Type u_1) [] :
= id
def ContinuousMap.const (α : Type u_1) {β : Type u_2} [] [] (b : β) :
C(α, β)

The constant map as a continuous map.

Equations
• = { toFun := fun (x : α) => b, continuous_toFun := }
Instances For
@[simp]
theorem ContinuousMap.coe_const (α : Type u_1) {β : Type u_2} [] [] (b : β) :
=
@[simp]
theorem ContinuousMap.constPi_apply (α : Type u_1) {β : Type u_2} [] :
= fun (b : β) =>
def ContinuousMap.constPi (α : Type u_1) {β : Type u_2} [] :
C(β, αβ)

Function.const α b as a bundled continuous function of b.

Equations
• = { toFun := fun (b : β) => , continuous_toFun := }
Instances For
instance ContinuousMap.instInhabited (α : Type u_1) {β : Type u_2} [] [] [] :
Equations
@[simp]
theorem ContinuousMap.id_apply {α : Type u_1} [] (a : α) :
a = a
@[simp]
theorem ContinuousMap.const_apply {α : Type u_1} {β : Type u_2} [] [] (b : β) (a : α) :
a = b
def ContinuousMap.comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} [] [] [] (f : C(β, γ)) (g : C(α, β)) :
C(α, γ)

The composition of continuous maps, as a continuous map.

Equations
• f.comp g = { toFun := f g, continuous_toFun := }
Instances For
@[simp]
theorem ContinuousMap.coe_comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} [] [] [] (f : C(β, γ)) (g : C(α, β)) :
(f.comp g) = f g
@[simp]
theorem ContinuousMap.comp_apply {α : Type u_1} {β : Type u_2} {γ : Type u_3} [] [] [] (f : C(β, γ)) (g : C(α, β)) (a : α) :
(f.comp g) a = f (g a)
@[simp]
theorem ContinuousMap.comp_assoc {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} [] [] [] [] (f : C(γ, δ)) (g : C(β, γ)) (h : C(α, β)) :
(f.comp g).comp h = f.comp (g.comp h)
@[simp]
theorem ContinuousMap.id_comp {α : Type u_1} {β : Type u_2} [] [] (f : C(α, β)) :
.comp f = f
@[simp]
theorem ContinuousMap.comp_id {α : Type u_1} {β : Type u_2} [] [] (f : C(α, β)) :
f.comp = f
@[simp]
theorem ContinuousMap.const_comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} [] [] [] (c : γ) (f : C(α, β)) :
.comp f =
@[simp]
theorem ContinuousMap.comp_const {α : Type u_1} {β : Type u_2} {γ : Type u_3} [] [] [] (f : C(β, γ)) (b : β) :
f.comp = ContinuousMap.const α (f b)
@[simp]
theorem ContinuousMap.cancel_right {α : Type u_1} {β : Type u_2} {γ : Type u_3} [] [] [] {f₁ : C(β, γ)} {f₂ : C(β, γ)} {g : C(α, β)} (hg : ) :
f₁.comp g = f₂.comp g f₁ = f₂
@[simp]
theorem ContinuousMap.cancel_left {α : Type u_1} {β : Type u_2} {γ : Type u_3} [] [] [] {f : C(β, γ)} {g₁ : C(α, β)} {g₂ : C(α, β)} (hf : ) :
f.comp g₁ = f.comp g₂ g₁ = g₂
instance ContinuousMap.instNontrivialOfNonempty {α : Type u_1} {β : Type u_2} [] [] [] [] :
Equations
• =
@[simp]
theorem ContinuousMap.fst_apply {α : Type u_1} {β : Type u_2} [] [] :
ContinuousMap.fst = Prod.fst
def ContinuousMap.fst {α : Type u_1} {β : Type u_2} [] [] :
C(α × β, α)

Prod.fst : (x, y) ↦ x as a bundled continuous map.

Equations
• ContinuousMap.fst = { toFun := Prod.fst, continuous_toFun := }
Instances For
@[simp]
theorem ContinuousMap.snd_apply {α : Type u_1} {β : Type u_2} [] [] :
ContinuousMap.snd = Prod.snd
def ContinuousMap.snd {α : Type u_1} {β : Type u_2} [] [] :
C(α × β, β)

Prod.snd : (x, y) ↦ y as a bundled continuous map.

Equations
• ContinuousMap.snd = { toFun := Prod.snd, continuous_toFun := }
Instances For
def ContinuousMap.prodMk {α : Type u_1} [] {β₁ : Type u_7} {β₂ : Type u_8} [] [] (f : C(α, β₁)) (g : C(α, β₂)) :
C(α, β₁ × β₂)

Given two continuous maps f and g, this is the continuous map x ↦ (f x, g x).

Equations
• f.prodMk g = { toFun := fun (x : α) => (f x, g x), continuous_toFun := }
Instances For
@[simp]
theorem ContinuousMap.prodMap_apply {α₁ : Type u_5} {α₂ : Type u_6} {β₁ : Type u_7} {β₂ : Type u_8} [] [] [] [] (f : C(α₁, α₂)) (g : C(β₁, β₂)) :
∀ (a : α₁ × β₁), (f.prodMap g) a = Prod.map (⇑f) (⇑g) a
def ContinuousMap.prodMap {α₁ : Type u_5} {α₂ : Type u_6} {β₁ : Type u_7} {β₂ : Type u_8} [] [] [] [] (f : C(α₁, α₂)) (g : C(β₁, β₂)) :
C(α₁ × β₁, α₂ × β₂)

Given two continuous maps f and g, this is the continuous map (x, y) ↦ (f x, g y).

Equations
• f.prodMap g = { toFun := Prod.map f g, continuous_toFun := }
Instances For
@[simp]
theorem ContinuousMap.prod_eval {α : Type u_1} [] {β₁ : Type u_7} {β₂ : Type u_8} [] [] (f : C(α, β₁)) (g : C(α, β₂)) (a : α) :
(f.prodMk g) a = (f a, g a)
@[simp]
theorem ContinuousMap.prodSwap_apply {α : Type u_1} {β : Type u_2} [] [] (x : α × β) :
ContinuousMap.prodSwap x = (x.2, x.1)
def ContinuousMap.prodSwap {α : Type u_1} {β : Type u_2} [] [] :
C(α × β, β × α)

Prod.swap bundled as a ContinuousMap.

Equations
• ContinuousMap.prodSwap = ContinuousMap.snd.prodMk ContinuousMap.fst
Instances For
@[simp]
theorem ContinuousMap.sigmaMk_apply {I : Type u_5} {X : IType u_7} [(i : I) → TopologicalSpace (X i)] (i : I) (snd : X i) :
snd = i, snd
def ContinuousMap.sigmaMk {I : Type u_5} {X : IType u_7} [(i : I) → TopologicalSpace (X i)] (i : I) :
C(X i, (i : I) × X i)

Sigma.mk i as a bundled continuous map.

Equations
• = { toFun := , continuous_toFun := }
Instances For
@[simp]
theorem ContinuousMap.sigma_apply {I : Type u_5} {A : Type u_6} {X : IType u_7} [] [(i : I) → TopologicalSpace (X i)] (f : (i : I) → C(X i, A)) (ig : (i : I) × X i) :
ig = (f ig.fst) ig.snd
def ContinuousMap.sigma {I : Type u_5} {A : Type u_6} {X : IType u_7} [] [(i : I) → TopologicalSpace (X i)] (f : (i : I) → C(X i, A)) :
C((i : I) × X i, A)

To give a continuous map out of a disjoint union, it suffices to give a continuous map out of each term. This is Sigma.uncurry for continuous maps.

Equations
• = { toFun := fun (ig : (i : I) × X i) => (f ig.fst) ig.snd, continuous_toFun := }
Instances For
@[simp]
theorem ContinuousMap.sigmaEquiv_apply {I : Type u_5} (A : Type u_6) (X : IType u_7) [] [(i : I) → TopologicalSpace (X i)] (f : (i : I) → C(X i, A)) :
@[simp]
theorem ContinuousMap.sigmaEquiv_symm_apply {I : Type u_5} (A : Type u_6) (X : IType u_7) [] [(i : I) → TopologicalSpace (X i)] (f : C((i : I) × X i, A)) (i : I) :
.symm f i = f.comp
def ContinuousMap.sigmaEquiv {I : Type u_5} (A : Type u_6) (X : IType u_7) [] [(i : I) → TopologicalSpace (X i)] :
((i : I) → C(X i, A)) C((i : I) × X i, A)

Giving a continuous map out of a disjoint union is the same as giving a continuous map out of each term. This is a version of Equiv.piCurry for continuous maps.

Equations
• = { toFun := ContinuousMap.sigma, invFun := fun (f : C((i : I) × X i, A)) (i : I) => f.comp , left_inv := , right_inv := }
Instances For
def ContinuousMap.pi {I : Type u_5} {A : Type u_6} {X : IType u_7} [] [(i : I) → TopologicalSpace (X i)] (f : (i : I) → C(A, X i)) :
C(A, (i : I) → X i)

Abbreviation for product of continuous maps, which is continuous

Equations
• = { toFun := fun (a : A) (i : I) => (f i) a, continuous_toFun := }
Instances For
@[simp]
theorem ContinuousMap.pi_eval {I : Type u_5} {A : Type u_6} {X : IType u_7} [] [(i : I) → TopologicalSpace (X i)] (f : (i : I) → C(A, X i)) (a : A) :
a = fun (i : I) => (f i) a
@[simp]
theorem ContinuousMap.eval_apply {I : Type u_5} {X : IType u_7} [(i : I) → TopologicalSpace (X i)] (i : I) :
def ContinuousMap.eval {I : Type u_5} {X : IType u_7} [(i : I) → TopologicalSpace (X i)] (i : I) :
C((j : I) → X j, X i)

Evaluation at point as a bundled continuous map.

Equations
• = { toFun := , continuous_toFun := }
Instances For
@[simp]
theorem ContinuousMap.piEquiv_apply {I : Type u_5} (A : Type u_6) (X : IType u_7) [] [(i : I) → TopologicalSpace (X i)] (f : (i : I) → C(A, X i)) :
f =
@[simp]
theorem ContinuousMap.piEquiv_symm_apply {I : Type u_5} (A : Type u_6) (X : IType u_7) [] [(i : I) → TopologicalSpace (X i)] (f : C(A, (i : I) → X i)) (i : I) :
.symm f i = .comp f
def ContinuousMap.piEquiv {I : Type u_5} (A : Type u_6) (X : IType u_7) [] [(i : I) → TopologicalSpace (X i)] :
((i : I) → C(A, X i)) C(A, (i : I) → X i)

Giving a continuous map out of a disjoint union is the same as giving a continuous map out of each term

Equations
• = { toFun := ContinuousMap.pi, invFun := fun (f : C(A, (i : I) → X i)) (i : I) => .comp f, left_inv := , right_inv := }
Instances For
@[simp]
theorem ContinuousMap.piMap_apply {I : Type u_5} {X : IType u_7} {Y : IType u_8} [(i : I) → TopologicalSpace (X i)] [(i : I) → TopologicalSpace (Y i)] (f : (i : I) → C(X i, Y i)) (a : (i : I) → X i) (i : I) :
a i = (f i) (a i)
def ContinuousMap.piMap {I : Type u_5} {X : IType u_7} {Y : IType u_8} [(i : I) → TopologicalSpace (X i)] [(i : I) → TopologicalSpace (Y i)] (f : (i : I) → C(X i, Y i)) :
C((i : I) → X i, (i : I) → Y i)

Combine a collection of bundled continuous maps C(X i, Y i) into a bundled continuous map C(∀ i, X i, ∀ i, Y i).

Equations
Instances For
def ContinuousMap.precomp {I : Type u_5} {X : IType u_7} [(i : I) → TopologicalSpace (X i)] {ι : Type u_9} (φ : ιI) :
C((i : I) → X i, (i : ι) → X (φ i))

"Precomposition" as a continuous map between dependent types.

Equations
• = { toFun := fun (f : (i : I) → X i) (j : ι) => f (φ j), continuous_toFun := }
Instances For
def ContinuousMap.restrict {α : Type u_1} {β : Type u_2} [] [] (s : Set α) (f : C(α, β)) :
C(s, β)

The restriction of a continuous function α → β to a subset s of α.

Equations
• = { toFun := f Subtype.val, continuous_toFun := }
Instances For
@[simp]
theorem ContinuousMap.coe_restrict {α : Type u_1} {β : Type u_2} [] [] (s : Set α) (f : C(α, β)) :
= f Subtype.val
@[simp]
theorem ContinuousMap.restrict_apply {α : Type u_1} {β : Type u_2} [] [] (f : C(α, β)) (s : Set α) (x : s) :
x = f x
@[simp]
theorem ContinuousMap.restrict_apply_mk {α : Type u_1} {β : Type u_2} [] [] (f : C(α, β)) (s : Set α) (x : α) (hx : x s) :
x, hx = f x
theorem ContinuousMap.injective_restrict {α : Type u_1} {β : Type u_2} [] [] [] {s : Set α} (hs : ) :
@[simp]
theorem ContinuousMap.restrictPreimage_apply {α : Type u_1} {β : Type u_2} [] [] (f : C(α, β)) (s : Set β) :
∀ (a : (f ⁻¹' s)), (f.restrictPreimage s) a = s.restrictPreimage (⇑f) a
def ContinuousMap.restrictPreimage {α : Type u_1} {β : Type u_2} [] [] (f : C(α, β)) (s : Set β) :
C((f ⁻¹' s), s)

The restriction of a continuous map to the preimage of a set.

Equations
• f.restrictPreimage s = { toFun := s.restrictPreimage f, continuous_toFun := }
Instances For
noncomputable def ContinuousMap.liftCover {α : Type u_1} {β : Type u_2} [] [] {ι : Type u_5} (S : ιSet α) (φ : (i : ι) → C((S i), β)) (hφ : ∀ (i j : ι) (x : α) (hxi : x S i) (hxj : x S j), (φ i) x, hxi = (φ j) x, hxj) (hS : ∀ (x : α), ∃ (i : ι), S i nhds x) :
C(α, β)

A family φ i of continuous maps C(S i, β), where the domains S i contain a neighbourhood of each point in α and the functions φ i agree pairwise on intersections, can be glued to construct a continuous map in C(α, β).

Equations
Instances For
@[simp]
theorem ContinuousMap.liftCover_coe {α : Type u_1} {β : Type u_2} [] [] {ι : Type u_5} {S : ιSet α} {φ : (i : ι) → C((S i), β)} {hφ : ∀ (i j : ι) (x : α) (hxi : x S i) (hxj : x S j), (φ i) x, hxi = (φ j) x, hxj} {hS : ∀ (x : α), ∃ (i : ι), S i nhds x} {i : ι} (x : (S i)) :
(ContinuousMap.liftCover S φ hS) x = (φ i) x
theorem ContinuousMap.liftCover_restrict {α : Type u_1} {β : Type u_2} [] [] {ι : Type u_5} {S : ιSet α} {φ : (i : ι) → C((S i), β)} {hφ : ∀ (i j : ι) (x : α) (hxi : x S i) (hxj : x S j), (φ i) x, hxi = (φ j) x, hxj} {hS : ∀ (x : α), ∃ (i : ι), S i nhds x} {i : ι} :
noncomputable def ContinuousMap.liftCover' {α : Type u_1} {β : Type u_2} [] [] (A : Set (Set α)) (F : (s : Set α) → s AC(s, β)) (hF : ∀ (s : Set α) (hs : s A) (t : Set α) (ht : t A) (x : α) (hxi : x s) (hxj : x t), (F s hs) x, hxi = (F t ht) x, hxj) (hA : ∀ (x : α), iA, i nhds x) :
C(α, β)

A family F s of continuous maps C(s, β), where (1) the domains s are taken from a set A of sets in α which contain a neighbourhood of each point in α and (2) the functions F s agree pairwise on intersections, can be glued to construct a continuous map in C(α, β).

Equations
Instances For
@[simp]
theorem ContinuousMap.liftCover_coe' {α : Type u_1} {β : Type u_2} [] [] {A : Set (Set α)} {F : (s : Set α) → s AC(s, β)} {hF : ∀ (s : Set α) (hs : s A) (t : Set α) (ht : t A) (x : α) (hxi : x s) (hxj : x t), (F s hs) x, hxi = (F t ht) x, hxj} {hA : ∀ (x : α), iA, i nhds x} {s : Set α} {hs : s A} (x : s) :
(ContinuousMap.liftCover' A F hF hA) x = (F s hs) x
@[simp]
theorem ContinuousMap.liftCover_restrict' {α : Type u_1} {β : Type u_2} [] [] {A : Set (Set α)} {F : (s : Set α) → s AC(s, β)} {hF : ∀ (s : Set α) (hs : s A) (t : Set α) (ht : t A) (x : α) (hxi : x s) (hxj : x t), (F s hs) x, hxi = (F t ht) x, hxj} {hA : ∀ (x : α), iA, i nhds x} {s : Set α} {hs : s A} :
@[simp]
theorem Function.RightInverse.homeomorph_symm_apply {X : Type u_1} {Y : Type u_2} [] [] {f : C(X, Y)} {f' : C(Y, X)} (hf : ) (b : Y) :
hf.homeomorph.symm b = Quotient.mk'' (f' b)
@[simp]
theorem Function.RightInverse.homeomorph_apply {X : Type u_1} {Y : Type u_2} [] [] {f : C(X, Y)} {f' : C(Y, X)} (hf : ) (a : Quotient (Setoid.ker f)) :
hf.homeomorph a = a.liftOn' f
def Function.RightInverse.homeomorph {X : Type u_1} {Y : Type u_2} [] [] {f : C(X, Y)} {f' : C(Y, X)} (hf : ) :

Setoid.quotientKerEquivOfRightInverse as a homeomorphism.

Equations
Instances For
@[simp]
theorem QuotientMap.homeomorph_symm_apply {X : Type u_1} {Y : Type u_2} [] [] {f : C(X, Y)} (hf : ) (b : Y) :
hf.homeomorph.symm b =
@[simp]
theorem QuotientMap.homeomorph_apply {X : Type u_1} {Y : Type u_2} [] [] {f : C(X, Y)} (hf : ) (a : Quotient (Setoid.ker f)) :
hf.homeomorph a = a.liftOn' f
noncomputable def QuotientMap.homeomorph {X : Type u_1} {Y : Type u_2} [] [] {f : C(X, Y)} (hf : ) :

The homeomorphism from the quotient of a quotient map to its codomain. This is Setoid.quotientKerEquivOfSurjective as a homeomorphism.

Equations
• hf.homeomorph = { toEquiv := , continuous_toFun := , continuous_invFun := }
Instances For
@[simp]
theorem QuotientMap.lift_apply {X : Type u_1} {Y : Type u_2} {Z : Type u_3} [] [] [] {f : C(X, Y)} (hf : ) (g : C(X, Z)) (h : ) :
∀ (a : Y), (hf.lift g h) a = ((fun (i : Quotient (Setoid.ker f)) => i.liftOn' g ) hf.homeomorph.symm) a
noncomputable def QuotientMap.lift {X : Type u_1} {Y : Type u_2} {Z : Type u_3} [] [] [] {f : C(X, Y)} (hf : ) (g : C(X, Z)) (h : ) :
C(Y, Z)

Descend a continuous map, which is constant on the fibres, along a quotient map.

Equations
• hf.lift g h = { toFun := (fun (i : Quotient (Setoid.ker f)) => i.liftOn' g ) hf.homeomorph.symm, continuous_toFun := }
Instances For
@[simp]
theorem QuotientMap.lift_comp {X : Type u_1} {Y : Type u_2} {Z : Type u_3} [] [] [] {f : C(X, Y)} (hf : ) (g : C(X, Z)) (h : ) :
(hf.lift g h).comp f = g

The obvious triangle induced by QuotientMap.lift commutes:

     g
X --→ Z
|   ↗
f |  / hf.lift g h
v /
Y

@[simp]
theorem QuotientMap.liftEquiv_symm_apply_coe {X : Type u_1} {Y : Type u_2} {Z : Type u_3} [] [] [] {f : C(X, Y)} (hf : ) (g : C(Y, Z)) :
(hf.liftEquiv.symm g) = g.comp f
@[simp]
theorem QuotientMap.liftEquiv_apply {X : Type u_1} {Y : Type u_2} {Z : Type u_3} [] [] [] {f : C(X, Y)} (hf : ) (g : { g : C(X, Z) // }) :
hf.liftEquiv g = hf.lift g
noncomputable def QuotientMap.liftEquiv {X : Type u_1} {Y : Type u_2} {Z : Type u_3} [] [] [] {f : C(X, Y)} (hf : ) :
{ g : C(X, Z) // } C(Y, Z)

QuotientMap.lift as an equivalence.

Equations
• hf.liftEquiv = { toFun := fun (g : { g : C(X, Z) // }) => hf.lift g , invFun := fun (g : C(Y, Z)) => g.comp f, , left_inv := , right_inv := }
Instances For
@[simp]
theorem Homeomorph.toContinuousMap_apply {α : Type u_1} {β : Type u_2} [] [] (e : α ≃ₜ β) (a : α) :
e.toContinuousMap a = e a
def Homeomorph.toContinuousMap {α : Type u_1} {β : Type u_2} [] [] (e : α ≃ₜ β) :
C(α, β)

The forward direction of a homeomorphism, as a bundled continuous map.

Equations
• e.toContinuousMap = { toFun := e, continuous_toFun := }
Instances For
instance Homeomorph.instCoeContinuousMap {α : Type u_1} {β : Type u_2} [] [] :
Coe (α ≃ₜ β) C(α, β)

Homeomorph.toContinuousMap as a coercion.

Equations
• Homeomorph.instCoeContinuousMap = { coe := Homeomorph.toContinuousMap }
@[simp]
theorem Homeomorph.coe_refl {α : Type u_1} [] :
.toContinuousMap =
@[simp]
theorem Homeomorph.coe_trans {α : Type u_1} {β : Type u_2} {γ : Type u_3} [] [] [] (f : α ≃ₜ β) (g : β ≃ₜ γ) :
(f.trans g).toContinuousMap = g.toContinuousMap.comp f.toContinuousMap
@[simp]
theorem Homeomorph.symm_comp_toContinuousMap {α : Type u_1} {β : Type u_2} [] [] (f : α ≃ₜ β) :
f.symm.toContinuousMap.comp f.toContinuousMap =

Left inverse to a continuous map from a homeomorphism, mirroring Equiv.symm_comp_self.

@[simp]
theorem Homeomorph.toContinuousMap_comp_symm {α : Type u_1} {β : Type u_2} [] [] (f : α ≃ₜ β) :
f.toContinuousMap.comp f.symm.toContinuousMap =

Right inverse to a continuous map from a homeomorphism, mirroring Equiv.self_comp_symm.