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.

theorem map_continuousAt {F : Type u_1} {α : Type u_2} {β : Type u_3} [TopologicalSpace α] [TopologicalSpace β] [FunLike F α β] [ContinuousMapClass F α β] (f : F) (a : α) : ContinuousAt (⇑f) a

theorem map_continuousWithinAt {F : Type u_1} {α : Type u_2} {β : Type u_3} [TopologicalSpace α] [TopologicalSpace β] [FunLike F α β] [ContinuousMapClass F α β] (f : F) (s : Set α) (a : α) : ContinuousWithinAt (⇑f) s a

Continuous maps

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

Deprecated. Use map_continuousAt instead.

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

def ContinuousMap.equivFnOfDiscrete {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] [DiscreteTopology α] : C(α, β) ≃ (α → β)

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

@[simp]

theorem ContinuousMap.equivFnOfDiscrete_apply {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] [DiscreteTopology α] (f : C(α, β)) (a : α) : equivFnOfDiscrete f a = f a

@[simp]

theorem ContinuousMap.equivFnOfDiscrete_symm_apply_apply {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] [DiscreteTopology α] (f : α → β) (a✝ : α) : (equivFnOfDiscrete.symm f) a✝ = f a✝

@[simp]

theorem ContinuousMap.coe_equivFnOfDiscrete {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] [DiscreteTopology α] : ⇑equivFnOfDiscrete = DFunLike.coe

@[simp]

theorem ContinuousMap.equivFnOfDiscrete_symm_apply {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] [DiscreteTopology α] (f : α → β) : ⇑(equivFnOfDiscrete.symm f) = f

def ContinuousMap.id (α : Type u_1) [TopologicalSpace α] : C(α, α)

The identity as a continuous map.

@[simp]

theorem ContinuousMap.coe_id (α : Type u_1) [TopologicalSpace α] : ⇑(ContinuousMap.id α) = id

def ContinuousMap.const (α : Type u_1) {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] (b : β) : C(α, β)

The constant map as a continuous map.

@[simp]

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

def ContinuousMap.constPi (α : Type u_1) {β : Type u_2} [TopologicalSpace β] : C(β, α → β)

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

@[simp]

theorem ContinuousMap.constPi_apply (α : Type u_1) {β : Type u_2} [TopologicalSpace β] : ⇑(constPi α) = fun (b : β) => Function.const α b

instance ContinuousMap.instInhabited (α : Type u_1) {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] [Inhabited β] : Inhabited C(α, β)

@[simp]

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

@[simp]

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

def ContinuousMap.comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} [TopologicalSpace α] [TopologicalSpace β] [TopologicalSpace γ] (f : C(β, γ)) (g : C(α, β)) : C(α, γ)

The composition of continuous maps, as a continuous map.

@[simp]

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

@[simp]

theorem ContinuousMap.comp_apply {α : Type u_1} {β : Type u_2} {γ : Type u_3} [TopologicalSpace α] [TopologicalSpace β] [TopologicalSpace γ] (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} [TopologicalSpace α] [TopologicalSpace β] [TopologicalSpace γ] [TopologicalSpace δ] (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} [TopologicalSpace α] [TopologicalSpace β] (f : C(α, β)) : (ContinuousMap.id β).comp f = f

@[simp]

theorem ContinuousMap.comp_id {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] (f : C(α, β)) : f.comp (ContinuousMap.id α) = f

@[simp]

theorem ContinuousMap.const_comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} [TopologicalSpace α] [TopologicalSpace β] [TopologicalSpace γ] (c : γ) (f : C(α, β)) : (const β c).comp f = const α c

@[simp]

theorem ContinuousMap.comp_const {α : Type u_1} {β : Type u_2} {γ : Type u_3} [TopologicalSpace α] [TopologicalSpace β] [TopologicalSpace γ] (f : C(β, γ)) (b : β) : f.comp (const α b) = const α (f b)

@[simp]

theorem ContinuousMap.cancel_right {α : Type u_1} {β : Type u_2} {γ : Type u_3} [TopologicalSpace α] [TopologicalSpace β] [TopologicalSpace γ] {f₁ f₂ : C(β, γ)} {g : C(α, β)} (hg : Function.Surjective ⇑g) : f₁.comp g = f₂.comp g ↔ f₁ = f₂

@[simp]

theorem ContinuousMap.cancel_left {α : Type u_1} {β : Type u_2} {γ : Type u_3} [TopologicalSpace α] [TopologicalSpace β] [TopologicalSpace γ] {f : C(β, γ)} {g₁ g₂ : C(α, β)} (hf : Function.Injective ⇑f) : f.comp g₁ = f.comp g₂ ↔ g₁ = g₂

instance ContinuousMap.instNontrivialOfNonempty {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] [Nonempty α] [Nontrivial β] : Nontrivial C(α, β)

def ContinuousMap.fst {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] : C(α × β, α)

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

@[simp]

theorem ContinuousMap.fst_apply {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] : ⇑fst = Prod.fst

def ContinuousMap.snd {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] : C(α × β, β)

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

@[simp]

theorem ContinuousMap.snd_apply {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] : ⇑snd = Prod.snd

def ContinuousMap.prodMk {α : Type u_1} [TopologicalSpace α] {β₁ : Type u_7} {β₂ : Type u_8} [TopologicalSpace β₁] [TopologicalSpace β₂] (f : C(α, β₁)) (g : C(α, β₂)) : C(α, β₁ × β₂)

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

def ContinuousMap.prodMap {α₁ : Type u_5} {α₂ : Type u_6} {β₁ : Type u_7} {β₂ : Type u_8} [TopologicalSpace α₁] [TopologicalSpace α₂] [TopologicalSpace β₁] [TopologicalSpace β₂] (f : C(α₁, α₂)) (g : C(β₁, β₂)) : C(α₁ × β₁, α₂ × β₂)

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

@[simp]

theorem ContinuousMap.prodMap_apply {α₁ : Type u_5} {α₂ : Type u_6} {β₁ : Type u_7} {β₂ : Type u_8} [TopologicalSpace α₁] [TopologicalSpace α₂] [TopologicalSpace β₁] [TopologicalSpace β₂] (f : C(α₁, α₂)) (g : C(β₁, β₂)) (a✝ : α₁ × β₁) : (f.prodMap g) a✝ = Prod.map (⇑f) (⇑g) a✝

@[simp]

theorem ContinuousMap.prod_eval {α : Type u_1} [TopologicalSpace α] {β₁ : Type u_7} {β₂ : Type u_8} [TopologicalSpace β₁] [TopologicalSpace β₂] (f : C(α, β₁)) (g : C(α, β₂)) (a : α) : (f.prodMk g) a = (f a, g a)

def ContinuousMap.prodSwap {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] : C(α × β, β × α)

Prod.swap bundled as a ContinuousMap.

@[simp]

theorem ContinuousMap.prodSwap_apply {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] (x : α × β) : prodSwap x = (x.2, x.1)

def ContinuousMap.sigmaMk {I : Type u_5} {X : I → Type u_7} [(i : I) → TopologicalSpace (X i)] (i : I) : C(X i, (i : I) × X i)

Sigma.mk i as a bundled continuous map.

@[simp]

theorem ContinuousMap.sigmaMk_apply {I : Type u_5} {X : I → Type u_7} [(i : I) → TopologicalSpace (X i)] (i : I) (snd : X i) : (sigmaMk i) snd = ⟨i, snd⟩

def ContinuousMap.sigma {I : Type u_5} {A : Type u_6} {X : I → Type u_7} [TopologicalSpace A] [(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.

@[simp]

theorem ContinuousMap.sigma_apply {I : Type u_5} {A : Type u_6} {X : I → Type u_7} [TopologicalSpace A] [(i : I) → TopologicalSpace (X i)] (f : (i : I) → C(X i, A)) (ig : (i : I) × X i) : (sigma f) ig = (f ig.fst) ig.snd

def ContinuousMap.sigmaEquiv {I : Type u_5} (A : Type u_6) (X : I → Type u_7) [TopologicalSpace A] [(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.

@[simp]

theorem ContinuousMap.sigmaEquiv_apply {I : Type u_5} (A : Type u_6) (X : I → Type u_7) [TopologicalSpace A] [(i : I) → TopologicalSpace (X i)] (f : (i : I) → C(X i, A)) : (sigmaEquiv A X) f = sigma f

@[simp]

theorem ContinuousMap.sigmaEquiv_symm_apply {I : Type u_5} (A : Type u_6) (X : I → Type u_7) [TopologicalSpace A] [(i : I) → TopologicalSpace (X i)] (f : C((i : I) × X i, A)) (i : I) : (sigmaEquiv A X).symm f i = f.comp (sigmaMk i)

def ContinuousMap.pi {I : Type u_5} {A : Type u_6} {X : I → Type u_7} [TopologicalSpace A] [(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

@[simp]

theorem ContinuousMap.pi_eval {I : Type u_5} {A : Type u_6} {X : I → Type u_7} [TopologicalSpace A] [(i : I) → TopologicalSpace (X i)] (f : (i : I) → C(A, X i)) (a : A) : (pi f) a = fun (i : I) => (f i) a

def ContinuousMap.eval {I : Type u_5} {X : I → Type u_7} [(i : I) → TopologicalSpace (X i)] (i : I) : C((j : I) → X j, X i)

Evaluation at point as a bundled continuous map.

@[simp]

theorem ContinuousMap.eval_apply {I : Type u_5} {X : I → Type u_7} [(i : I) → TopologicalSpace (X i)] (i : I) : ⇑(eval i) = Function.eval i

def ContinuousMap.piEquiv {I : Type u_5} (A : Type u_6) (X : I → Type u_7) [TopologicalSpace A] [(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

@[simp]

theorem ContinuousMap.piEquiv_symm_apply {I : Type u_5} (A : Type u_6) (X : I → Type u_7) [TopologicalSpace A] [(i : I) → TopologicalSpace (X i)] (f : C(A, (i : I) → X i)) (i : I) : (piEquiv A X).symm f i = (eval i).comp f

@[simp]

theorem ContinuousMap.piEquiv_apply {I : Type u_5} (A : Type u_6) (X : I → Type u_7) [TopologicalSpace A] [(i : I) → TopologicalSpace (X i)] (f : (i : I) → C(A, X i)) : (piEquiv A X) f = pi f

def ContinuousMap.piMap {I : Type u_5} {X : I → Type u_7} {Y : I → Type 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).

@[simp]

theorem ContinuousMap.piMap_apply {I : Type u_5} {X : I → Type u_7} {Y : I → Type 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) : (piMap f) a i = (f i) (a i)

def ContinuousMap.precomp {I : Type u_5} {X : I → Type 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.

def ContinuousMap.restrict {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] (s : Set α) (f : C(α, β)) : C(↑s, β)

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

@[simp]

theorem ContinuousMap.coe_restrict {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] (s : Set α) (f : C(α, β)) : ⇑(restrict s f) = ⇑f ∘ Subtype.val

@[simp]

theorem ContinuousMap.restrict_apply {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] (f : C(α, β)) (s : Set α) (x : ↑s) : (restrict s f) x = f ↑x

@[simp]

theorem ContinuousMap.restrict_apply_mk {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] (f : C(α, β)) (s : Set α) (x : α) (hx : x ∈ s) : (restrict s f) ⟨x, hx⟩ = f x

theorem ContinuousMap.injective_restrict {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] [T2Space β] {s : Set α} (hs : Dense s) : Function.Injective (restrict s)

def ContinuousMap.restrictPreimage {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] (f : C(α, β)) (s : Set β) : C(↑(⇑f ⁻¹' s), ↑s)

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

@[simp]

theorem ContinuousMap.restrictPreimage_apply {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] (f : C(α, β)) (s : Set β) (a✝ : ↑(⇑f ⁻¹' s)) : (f.restrictPreimage s) a✝ = s.restrictPreimage (⇑f) a✝

noncomputable def ContinuousMap.mkD {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] (f : α → β) (default : C(α, β)) : C(α, β)

Interpret f : α → β as an element of C(α, β), falling back to the default value default : C(α, β) if f is not continuous. This is mainly intended to be used for C(α, β)-valued integration. For example, if a family of functions f : ι → α → β satisfies that f i is continuous for almost every i, you can write the C(α, β)-valued integral "∫ i, f i" as ∫ i, ContinuousMap.mkD (f i) 0.

theorem ContinuousMap.mkD_of_continuous {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {f : α → β} {g : C(α, β)} (hf : Continuous f) : mkD f g = { toFun := f, continuous_toFun := hf }

theorem ContinuousMap.mkD_of_not_continuous {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {f : α → β} {g : C(α, β)} (hf : ¬Continuous f) : mkD f g = g

theorem ContinuousMap.mkD_apply_of_continuous {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {f : α → β} {g : C(α, β)} {x : α} (hf : Continuous f) : (mkD f g) x = f x

theorem ContinuousMap.mkD_of_continuousOn {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {s : Set α} {f : α → β} {g : C(↑s, β)} (hf : ContinuousOn f s) : mkD (s.restrict f) g = { toFun := s.restrict f, continuous_toFun := ⋯ }

theorem ContinuousMap.mkD_of_not_continuousOn {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {s : Set α} {f : α → β} {g : C(↑s, β)} (hf : ¬ContinuousOn f s) : mkD (s.restrict f) g = g

theorem ContinuousMap.mkD_apply_of_continuousOn {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {s : Set α} {f : α → β} {g : C(↑s, β)} {x : ↑s} (hf : ContinuousOn f s) : (mkD (s.restrict f) g) x = f ↑x

theorem ContinuousMap.mkD_eq_self {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {f g : C(α, β)} : mkD (⇑f) g = f

noncomputable def ContinuousMap.liftCover {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {ι : 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(α, β).

@[simp]

theorem ContinuousMap.liftCover_coe {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {ι : 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)) : (liftCover S φ hφ hS) ↑x = (φ i) x

@[simp]

theorem ContinuousMap.liftCover_restrict {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {ι : 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 : ι} : restrict (S i) (liftCover S φ hφ hS) = φ i

noncomputable def ContinuousMap.liftCover' {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] (A : Set (Set α)) (F : (s : Set α) → s ∈ A → C(↑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 : α), ∃ i ∈ A, 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(α, β).

@[simp]

theorem ContinuousMap.liftCover_coe' {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {A : Set (Set α)} {F : (s : Set α) → s ∈ A → C(↑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 : α), ∃ i ∈ A, i ∈ nhds x} {s : Set α} {hs : s ∈ A} (x : ↑s) : (liftCover' A F hF hA) ↑x = (F s hs) x

@[simp]

theorem ContinuousMap.liftCover_restrict' {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {A : Set (Set α)} {F : (s : Set α) → s ∈ A → C(↑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 : α), ∃ i ∈ A, i ∈ nhds x} {s : Set α} {hs : s ∈ A} : restrict s (liftCover' A F hF hA) = F s hs

def ContinuousMap.inclusion {α : Type u_1} [TopologicalSpace α] {s t : Set α} (h : s ⊆ t) : C(↑s, ↑t)

Set.inclusion as a bundled continuous map.

def Function.RightInverse.homeomorph {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {f : C(X, Y)} {f' : C(Y, X)} (hf : RightInverse ⇑f' ⇑f) : Quotient (Setoid.ker ⇑f) ≃ₜ Y

Setoid.quotientKerEquivOfRightInverse as a homeomorphism.

@[simp]

theorem Function.RightInverse.homeomorph_symm_apply {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {f : C(X, Y)} {f' : C(Y, X)} (hf : RightInverse ⇑f' ⇑f) (b : Y) : hf.homeomorph.symm b = Quotient.mk'' (f' b)

@[simp]

theorem Function.RightInverse.homeomorph_apply {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {f : C(X, Y)} {f' : C(Y, X)} (hf : RightInverse ⇑f' ⇑f) (a : Quotient (Setoid.ker ⇑f)) : hf.homeomorph a = a.liftOn' ⇑f ⋯

noncomputable def Topology.IsQuotientMap.homeomorph {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {f : C(X, Y)} (hf : IsQuotientMap ⇑f) : Quotient (Setoid.ker ⇑f) ≃ₜ Y

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

@[simp]

theorem Topology.IsQuotientMap.homeomorph_symm_apply {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {f : C(X, Y)} (hf : IsQuotientMap ⇑f) (b : Y) : hf.homeomorph.symm b = Quotient.mk'' (Function.surjInv ⋯ b)

@[simp]

theorem Topology.IsQuotientMap.homeomorph_apply {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {f : C(X, Y)} (hf : IsQuotientMap ⇑f) (a : Quotient (Setoid.ker ⇑f)) : hf.homeomorph a = a.liftOn' ⇑f ⋯

noncomputable def Topology.IsQuotientMap.lift {X : Type u_1} {Y : Type u_2} {Z : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] [TopologicalSpace Z] {f : C(X, Y)} (hf : IsQuotientMap ⇑f) (g : C(X, Z)) (h : Function.FactorsThrough ⇑g ⇑f) : C(Y, Z)

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

@[simp]

theorem Topology.IsQuotientMap.lift_apply {X : Type u_1} {Y : Type u_2} {Z : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] [TopologicalSpace Z] {f : C(X, Y)} (hf : IsQuotientMap ⇑f) (g : C(X, Z)) (h : Function.FactorsThrough ⇑g ⇑f) (a✝ : Y) : (hf.lift g h) a✝ = ((fun (i : Quotient (Setoid.ker ⇑f)) => i.liftOn' ⇑g ⋯) ∘ ⇑hf.homeomorph.symm) a✝

@[simp]

theorem Topology.IsQuotientMap.lift_comp {X : Type u_1} {Y : Type u_2} {Z : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] [TopologicalSpace Z] {f : C(X, Y)} (hf : IsQuotientMap ⇑f) (g : C(X, Z)) (h : Function.FactorsThrough ⇑g ⇑f) : (hf.lift g h).comp f = g

The obvious triangle induced by IsQuotientMap.lift commutes:

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

noncomputable def Topology.IsQuotientMap.liftEquiv {X : Type u_1} {Y : Type u_2} {Z : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] [TopologicalSpace Z] {f : C(X, Y)} (hf : IsQuotientMap ⇑f) : { g : C(X, Z) // Function.FactorsThrough ⇑g ⇑f } ≃ C(Y, Z)

IsQuotientMap.lift as an equivalence.

@[simp]

theorem Topology.IsQuotientMap.liftEquiv_symm_apply_coe {X : Type u_1} {Y : Type u_2} {Z : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] [TopologicalSpace Z] {f : C(X, Y)} (hf : IsQuotientMap ⇑f) (g : C(Y, Z)) : ↑(hf.liftEquiv.symm g) = g.comp f

@[simp]

theorem Topology.IsQuotientMap.liftEquiv_apply {X : Type u_1} {Y : Type u_2} {Z : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] [TopologicalSpace Z] {f : C(X, Y)} (hf : IsQuotientMap ⇑f) (g : { g : C(X, Z) // Function.FactorsThrough ⇑g ⇑f }) : hf.liftEquiv g = hf.lift ↑g ⋯

instance Homeomorph.instContinuousMapClass {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] : ContinuousMapClass (α ≃ₜ β) α β

@[simp]

theorem Homeomorph.coe_refl {α : Type u_1} [TopologicalSpace α] : ↑(Homeomorph.refl α) = ContinuousMap.id α

@[simp]

theorem Homeomorph.coe_trans {α : Type u_1} {β : Type u_2} {γ : Type u_3} [TopologicalSpace α] [TopologicalSpace β] [TopologicalSpace γ] (f : α ≃ₜ β) (g : β ≃ₜ γ) : ↑(f.trans g) = (↑g).comp ↑f

@[simp]

theorem Homeomorph.symm_comp_toContinuousMap {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] (f : α ≃ₜ β) : (↑f.symm).comp ↑f = ContinuousMap.id α

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} [TopologicalSpace α] [TopologicalSpace β] (f : α ≃ₜ β) : (↑f).comp ↑f.symm = ContinuousMap.id β

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