# 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.

source
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
source
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 #

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

Deprecated. Use `map_continuousAt` instead.

source
theorem ContinuousMap.map_specializes {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] (f : C(α, β)) {x y : α} (h : x ⤳ y) :
f x ⤳ f y
source
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.

Equations

- ContinuousMap.equivFnOfDiscrete = { toFun := fun (f : C(α, β)) => ⇑f, invFun := fun (f : α → β) => { toFun := f, continuous_toFun := ⋯ }, left_inv := ⋯, right_inv := ⋯ }

Instances For

source
@[simp]
theorem ContinuousMap.equivFnOfDiscrete_apply {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] [DiscreteTopology α] (f : C(α, β)) (a : α) :
equivFnOfDiscrete f a = f a
source
@[simp]
theorem ContinuousMap.equivFnOfDiscrete_symm_apply_apply {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] [DiscreteTopology α] (f : α → β) (a✝ : α) :
(equivFnOfDiscrete.symm f) a✝ = f a✝
source
@[simp]
theorem ContinuousMap.coe_equivFnOfDiscrete {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] [DiscreteTopology α] :
⇑equivFnOfDiscrete = DFunLike.coe
source
@[simp]
theorem ContinuousMap.equivFnOfDiscrete_symm_apply {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] [DiscreteTopology α] (f : α → β) :
⇑(equivFnOfDiscrete.symm f) = f
source
def ContinuousMap.id (α : Type u_1) [TopologicalSpace α] :
C(α, α)

The identity as a continuous map.

Equations

- ContinuousMap.id α = { toFun := id, continuous_toFun := ⋯ }

Instances For

source
@[simp]
theorem ContinuousMap.coe_id (α : Type u_1) [TopologicalSpace α] :
⇑(ContinuousMap.id α) = id
source
def ContinuousMap.const (α : Type u_1) {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] (b : β) :
C(α, β)

The constant map as a continuous map.

Equations

- ContinuousMap.const α b = { toFun := fun (x : α) => b, continuous_toFun := ⋯ }

Instances For

source
@[simp]
theorem ContinuousMap.coe_const (α : Type u_1) {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] (b : β) :
⇑(const α b) = Function.const α b
source
def ContinuousMap.constPi (α : Type u_1) {β : Type u_2} [TopologicalSpace β] :
C(β, α → β)

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

Equations

- ContinuousMap.constPi α = { toFun := fun (b : β) => Function.const α b, continuous_toFun := ⋯ }

Instances For

source
@[simp]
theorem ContinuousMap.constPi_apply (α : Type u_1) {β : Type u_2} [TopologicalSpace β] :
⇑(constPi α) = fun (b : β) => Function.const α b
source
instance ContinuousMap.instInhabited (α : Type u_1) {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] [Inhabited β] :
Inhabited C(α, β)
Equations

- ContinuousMap.instInhabited α = { default := ContinuousMap.const α default }

source
@[simp]
theorem ContinuousMap.id_apply {α : Type u_1} [TopologicalSpace α] (a : α) :
(ContinuousMap.id α) a = a
source
@[simp]
theorem ContinuousMap.const_apply {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] (b : β) (a : α) :
(const α b) a = b
source
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.

Equations

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

Instances For

source
@[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
source
@[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)
source
@[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)
source
@[simp]
theorem ContinuousMap.id_comp {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] (f : C(α, β)) :
(ContinuousMap.id β).comp f = f
source
@[simp]
theorem ContinuousMap.comp_id {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] (f : C(α, β)) :
f.comp (ContinuousMap.id α) = f
source
@[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
source
@[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)
source
@[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₂
source
@[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₂
source
instance ContinuousMap.instNontrivialOfNonempty {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] [Nonempty α] [Nontrivial β] :
Nontrivial C(α, β)
source
def Homeomorph.continuousMapCongr {X₁ : Type u_5} {X₂ : Type u_6} {Y₁ : Type u_7} {Y₂ : Type u_8} [TopologicalSpace X₁] [TopologicalSpace X₂] [TopologicalSpace Y₁] [TopologicalSpace Y₂] (e : X₁ ≃ₜ X₂) (e' : Y₁ ≃ₜ Y₂) :
C(X₁, Y₁) ≃ C(X₂, Y₂)

The bijection `C(X₁, Y₁) ≃ C(X₂, Y₂)` induced by homeomorphisms `e : X₁ ≃ₜ X₂` and `e' : Y₁ ≃ₜ Y₂`.

Equations

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

Instances For

source
@[simp]
theorem Homeomorph.continuousMapCongr_symm_apply {X₁ : Type u_5} {X₂ : Type u_6} {Y₁ : Type u_7} {Y₂ : Type u_8} [TopologicalSpace X₁] [TopologicalSpace X₂] [TopologicalSpace Y₁] [TopologicalSpace Y₂] (e : X₁ ≃ₜ X₂) (e' : Y₁ ≃ₜ Y₂) (g : C(X₂, Y₂)) :
(e.continuousMapCongr e').symm g = { toFun := ⇑e'.symm, continuous_toFun := ⋯ }.comp (g.comp { toFun := ⇑e, continuous_toFun := ⋯ })
source
@[simp]
theorem Homeomorph.continuousMapCongr_apply {X₁ : Type u_5} {X₂ : Type u_6} {Y₁ : Type u_7} {Y₂ : Type u_8} [TopologicalSpace X₁] [TopologicalSpace X₂] [TopologicalSpace Y₁] [TopologicalSpace Y₂] (e : X₁ ≃ₜ X₂) (e' : Y₁ ≃ₜ Y₂) (f : C(X₁, Y₁)) :
(e.continuousMapCongr e') f = { toFun := ⇑e', continuous_toFun := ⋯ }.comp (f.comp { toFun := ⇑e.symm, continuous_toFun := ⋯ })
source
def ContinuousMap.fst {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] :
C(α × β, α)

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

Equations

- ContinuousMap.fst = { toFun := Prod.fst, continuous_toFun := ⋯ }

Instances For

source
@[simp]
theorem ContinuousMap.fst_apply {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] :
⇑fst = Prod.fst
source
def ContinuousMap.snd {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] :
C(α × β, β)

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

Equations

- ContinuousMap.snd = { toFun := Prod.snd, continuous_toFun := ⋯ }

Instances For

source
@[simp]
theorem ContinuousMap.snd_apply {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] :
⇑snd = Prod.snd
source
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)`.

Equations

- f.prodMk g = { toFun := fun (x : α) => (f x, g x), continuous_toFun := ⋯ }

Instances For

source
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)`.

Equations

- f.prodMap g = { toFun := Prod.map ⇑f ⇑g, continuous_toFun := ⋯ }

Instances For

source
@[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✝
source
@[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)
source
def ContinuousMap.prodSwap {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] :
C(α × β, β × α)

`Prod.swap` bundled as a `ContinuousMap`.

Equations

- ContinuousMap.prodSwap = ContinuousMap.snd.prodMk ContinuousMap.fst

Instances For

source
@[simp]
theorem ContinuousMap.prodSwap_apply {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] (x : α × β) :
prodSwap x = (x.2, x.1)
source
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.

Equations

- ContinuousMap.sigmaMk i = { toFun := Sigma.mk i, continuous_toFun := ⋯ }

Instances For

source
@[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⟩
source
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.

Equations

- ContinuousMap.sigma f = { toFun := fun (ig : (i : I) × X i) => (f ig.fst) ig.snd, continuous_toFun := ⋯ }

Instances For

source
@[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
source
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.

Equations

- ContinuousMap.sigmaEquiv A X = { toFun := ContinuousMap.sigma, invFun := fun (f : C((i : I) × X i, A)) (i : I) => f.comp (ContinuousMap.sigmaMk i), left_inv := ⋯, right_inv := ⋯ }

Instances For

source
@[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)
source
@[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
source
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

Equations

- ContinuousMap.pi f = { toFun := fun (a : A) (i : I) => (f i) a, continuous_toFun := ⋯ }

Instances For

source
@[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
source
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.

Equations

- ContinuousMap.eval i = { toFun := Function.eval i, continuous_toFun := ⋯ }

Instances For

source
@[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
source
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

Equations

- ContinuousMap.piEquiv A X = { toFun := ContinuousMap.pi, invFun := fun (f : C(A, (i : I) → X i)) (i : I) => (ContinuousMap.eval i).comp f, left_inv := ⋯, right_inv := ⋯ }

Instances For

source
@[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
source
@[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
source
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)`.

Equations

- ContinuousMap.piMap f = ContinuousMap.pi fun (i : I) => (f i).comp (ContinuousMap.eval i)

Instances For

source
@[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)
source
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.

Equations

- ContinuousMap.precomp φ = { toFun := fun (f : (i : I) → X i) (j : ι) => f (φ j), continuous_toFun := ⋯ }

Instances For

source
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 `α`.

Equations

- ContinuousMap.restrict s f = { toFun := ⇑f ∘ Subtype.val, continuous_toFun := ⋯ }

Instances For

source
@[simp]
theorem ContinuousMap.coe_restrict {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] (s : Set α) (f : C(α, β)) :
⇑(restrict s f) = ⇑f ∘ Subtype.val
source
@[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
source
@[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
source
theorem ContinuousMap.injective_restrict {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] [T2Space β] {s : Set α} (hs : Dense s) :
Function.Injective (restrict s)
source
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.

Equations

- f.restrictPreimage s = { toFun := s.restrictPreimage ⇑f, continuous_toFun := ⋯ }

Instances For

source
@[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✝
source
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`.

Equations

- ContinuousMap.mkD f default = if h : Continuous f then { toFun := f, continuous_toFun := h } else default

Instances For

source
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 }
source
theorem ContinuousMap.mkD_of_not_continuous {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {f : α → β} {g : C(α, β)} (hf : ¬Continuous f) :
mkD f g = g
source
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
source
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 := ⋯ }
source
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
source
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
source
theorem ContinuousMap.mkD_eq_self {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {f g : C(α, β)} :
mkD (⇑f) g = f
source
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(α, β)`.

Equations

- ContinuousMap.liftCover S φ hφ hS = { toFun := Set.liftCover S (fun (i : ι) => ⇑(φ i)) hφ ⋯, continuous_toFun := ⋯ }

Instances For

source
@[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
source
@[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
source
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(α, β)`.

Equations

- ContinuousMap.liftCover' A F hF hA = ContinuousMap.liftCover Subtype.val (fun (i : ↑A) => F ↑i ⋯) ⋯ ⋯

Instances For

source
@[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
source
@[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
source
def ContinuousMap.inclusion {α : Type u_1} [TopologicalSpace α] {s t : Set α} (h : s ⊆ t) :
C(↑s, ↑t)

`Set.inclusion` as a bundled continuous map.

Equations

- ContinuousMap.inclusion h = { toFun := Set.inclusion h, continuous_toFun := ⋯ }

Instances For

source
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.

Equations

- hf.homeomorph = { toEquiv := Setoid.quotientKerEquivOfRightInverse (⇑f) (⇑f') hf, continuous_toFun := ⋯, continuous_invFun := ⋯ }

Instances For

source
@[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)
source
@[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✝ = Setoid.kerLift (⇑f) a✝
source
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.

Equations

- hf.homeomorph = { toEquiv := Setoid.quotientKerEquivOfSurjective ⇑f ⋯, continuous_toFun := ⋯, continuous_invFun := ⋯ }

Instances For

source
@[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)
source
@[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✝ = Setoid.kerLift (⇑f) a✝
source
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.

Equations

- hf.lift g h = { toFun := (fun (i : Quotient (Setoid.ker ⇑f)) => i.liftOn' ⇑g ⋯) ∘ ⇑hf.homeomorph.symm, continuous_toFun := ⋯ }

Instances For

source
@[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✝
source
@[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

source
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.

Equations

- hf.liftEquiv = { toFun := fun (g : { g : C(X, Z) // Function.FactorsThrough ⇑g ⇑f }) => hf.lift ↑g ⋯, invFun := fun (g : C(Y, Z)) => ⟨g.comp f, ⋯⟩, left_inv := ⋯, right_inv := ⋯ }

Instances For

source
@[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 ⋯
source
@[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
source
instance Homeomorph.instContinuousMapClass {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] :
ContinuousMapClass (α ≃ₜ β) α β
source
@[simp]
theorem Homeomorph.coe_refl {α : Type u_1} [TopologicalSpace α] :
↑(Homeomorph.refl α) = ContinuousMap.id α
source
@[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
source
@[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`.

source
@[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`.