Continuous bundled maps

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

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

• toFun : α → β

  The function α → β

• continuous_toFun : Continuous s.toFun

  Proposition that toFun is continuous

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.

def «termC(_,_)» : Lean.ParserDescr

The type of continuous maps from α to β.

Equations

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

class ContinuousMapClass (F : Type u_1) (α : outParam (Type u_2)) (β : outParam (Type u_3)) [TopologicalSpace α] [TopologicalSpace β] extends FunLike : Type (max (max u_1 u_2) u_3)

• coe : F → α → β
• coe_injective' : Function.Injective FunLike.coe
• map_continuous : ∀ (f : F), Continuous ↑f

  Continuity

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

You should extend this class when you extend ContinuousMap.

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

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

def toContinuousMap {F : Type u_1} {α : Type u_2} {β : Type u_3} [TopologicalSpace α] [TopologicalSpace β] [ContinuousMapClass F α β] (f : F) : C(α, β)

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

Equations

• ↑f = ContinuousMap.mk ↑f

instance instCoeTCContinuousMap {F : Type u_1} {α : Type u_2} {β : Type u_3} [TopologicalSpace α] [TopologicalSpace β] [ContinuousMapClass F α β] : CoeTC F C(α, β)

Equations

• instCoeTCContinuousMap = { coe := toContinuousMap }

Continuous maps

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

Equations

• ContinuousMap.toContinuousMapClass = ContinuousMapClass.mk (_ : ∀ (self : C(α, β)), Continuous self.toFun)

@[simp]

theorem ContinuousMap.toFun_eq_coe {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {f : C(α, β)} : f.toFun = ↑f

instance ContinuousMap.instCanLiftForAllContinuousMapCoeToFunLikeToContinuousMapClassContinuous {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] : CanLift (α → β) C(α, β) FunLike.coe Continuous

Equations

• @ContinuousMap.instCanLiftForAllContinuousMapCoeToFunLikeToContinuousMapClassContinuous = @ContinuousMap.instCanLiftForAllContinuousMapCoeToFunLikeToContinuousMapClassContinuous.proof_1

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

See note [custom simps projection].

Equations

• ContinuousMap.Simps.apply f = ↑f

@[simp]

theorem ContinuousMap.coe_coe {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {F : Type u_5} [ContinuousMapClass F α β] (f : F) : ↑↑f = ↑f

theorem ContinuousMap.ext {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {f : C(α, β)} {g : C(α, β)} (h : ∀ (a : α), ↑f a = ↑g a) : f = g

def ContinuousMap.copy {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] (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

• ContinuousMap.copy f f' h = ContinuousMap.mk f'

@[simp]

theorem ContinuousMap.coe_copy {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] (f : C(α, β)) (f' : α → β) (h : f' = ↑f) : ↑(ContinuousMap.copy f f' h) = f'

theorem ContinuousMap.copy_eq {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] (f : C(α, β)) (f' : α → β) (h : f' = ↑f) : ContinuousMap.copy f f' h = f

theorem ContinuousMap.continuous {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] (f : C(α, β)) : Continuous ↑f

Deprecated. Use map_continuous instead.

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

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

Deprecated. Use map_continuousAt instead.

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

Deprecated. Use FunLike.congr_fun instead.

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

Deprecated. Use FunLike.congr_arg instead.

theorem ContinuousMap.coe_injective {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] : Function.Injective FunLike.coe

@[simp]

theorem ContinuousMap.coe_mk {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] (f : α → β) (h : Continuous f) : ↑(ContinuousMap.mk f) = f

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

@[simp]

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

@[simp]

theorem ContinuousMap.equivFnOfDiscrete_symm_apply_apply (α : Type u_1) (β : Type u_2) [TopologicalSpace α] [TopologicalSpace β] [DiscreteTopology α] (f : α → β) : ∀ (a : α), ↑(↑(ContinuousMap.equivFnOfDiscrete α β).symm f) a = f a

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

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

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

The identity as a continuous map.

Equations

• ContinuousMap.id α = ContinuousMap.mk id

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

Equations

• ContinuousMap.const α b = ContinuousMap.mk fun x => b

@[simp]

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

@[simp]

theorem ContinuousMap.constPi_apply (α : Type u_1) {β : Type u_2} [TopologicalSpace β] : ↑(ContinuousMap.constPi α) = fun 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.

Equations

• ContinuousMap.constPi α = ContinuousMap.mk fun b => Function.const α b

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

Equations

• ContinuousMap.instInhabitedContinuousMap α = { default := ContinuousMap.const α default }

@[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 : α) : ↑(ContinuousMap.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.

Equations

• ContinuousMap.comp f g = ContinuousMap.mk (↑f ∘ ↑g)

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

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

Equations

• @ContinuousMap.instNontrivialContinuousMap = @ContinuousMap.instNontrivialContinuousMap.proof_1

@[simp]

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

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 = ContinuousMap.mk Prod.fst

@[simp]

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

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 = ContinuousMap.mk 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).

Equations

• ContinuousMap.prodMk f g = ContinuousMap.mk fun x => (↑f x, ↑g x)

@[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 : α₁ × β₁), ↑(ContinuousMap.prodMap f g) a = Prod.map (↑f) (↑g) a

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

• ContinuousMap.prodMap f g = ContinuousMap.mk (Prod.map ↑f ↑g)

@[simp]

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

@[simp]

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

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

Prod.swap bundled as a ContinuousMap.

Equations

• ContinuousMap.prodSwap = ContinuousMap.prodMk ContinuousMap.snd ContinuousMap.fst

@[simp]

theorem ContinuousMap.sigmaMk_apply {ι : Type u_5} {Y : ι → Type u_6} [(i : ι) → TopologicalSpace (Y i)] (i : ι) (snd : Y i) : ↑(ContinuousMap.sigmaMk i) snd = { fst := i, snd := snd }

def ContinuousMap.sigmaMk {ι : Type u_5} {Y : ι → Type u_6} [(i : ι) → TopologicalSpace (Y i)] (i : ι) : C(Y i, (i : ι) × Y i)

Sigma.mk i as a bundled continuous map.

Equations

• ContinuousMap.sigmaMk i = ContinuousMap.mk (Sigma.mk 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

Equations

• ContinuousMap.pi f = ContinuousMap.mk fun a i => ↑(f i) a

@[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) : ↑(ContinuousMap.pi f) a = fun i => ↑(f i) a

@[simp]

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

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 = ContinuousMap.mk (Function.eval 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) : ↑(ContinuousMap.piMap f) a i = ↑(f i) (a i)

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 => ContinuousMap.comp (f i) (ContinuousMap.eval 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.

Equations

• ContinuousMap.precomp φ = ContinuousMap.mk fun f j => f (φ j)

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 = ContinuousMap.mk (↑f ∘ Subtype.val)

@[simp]

theorem ContinuousMap.coe_restrict {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] (s : Set α) (f : C(α, β)) : ↑(ContinuousMap.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) : ↑(ContinuousMap.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) : ↑(ContinuousMap.restrict s f) { val := x, property := hx } = ↑f x

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

@[simp]

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

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

• ContinuousMap.restrictPreimage f s = ContinuousMap.mk (Set.restrictPreimage s ↑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) { val := x, property := hxi } = ↑(φ j) { val := x, property := 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 = ContinuousMap.mk (Set.liftCover S (fun i => ↑(φ i)) hφ (_ : ⋃ i, S i = Set.univ))

@[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) { val := x, property := hxi } = ↑(φ j) { val := x, property := hxj }} {hS : ∀ (x : α), ∃ i, S i ∈ nhds x} {i : ι} (x : ↑(S i)) : ↑(ContinuousMap.liftCover S φ hφ hS) ↑x = ↑(φ i) x

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) { val := x, property := hxi } = ↑(φ j) { val := x, property := hxj }} {hS : ∀ (x : α), ∃ i, S i ∈ nhds x} {i : ι} : ContinuousMap.restrict (S i) (ContinuousMap.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) { val := x, property := hxi } = ↑(F t ht) { val := x, property := hxj }) (hA : ∀ (x : α), ∃ i, 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

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

@[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) { val := x, property := hxi } = ↑(F t ht) { val := x, property := hxj }} {hA : ∀ (x : α), ∃ i, i ∈ A ∧ 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} [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) { val := x, property := hxi } = ↑(F t ht) { val := x, property := hxj }} {hA : ∀ (x : α), ∃ i, i ∈ A ∧ i ∈ nhds x} {s : Set α} {hs : s ∈ A} : ContinuousMap.restrict s (ContinuousMap.liftCover' A F hF hA) = F s hs

@[simp]

theorem Homeomorph.toContinuousMap_apply {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] (e : α ≃ₜ β) (a : α) : ↑(Homeomorph.toContinuousMap e) a = ↑e a

def Homeomorph.toContinuousMap {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] (e : α ≃ₜ β) : C(α, β)

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

Equations

• Homeomorph.toContinuousMap e = ContinuousMap.mk ↑e

instance Homeomorph.instCoeHomeomorphContinuousMap {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] : Coe (α ≃ₜ β) C(α, β)

Homeomorph.toContinuousMap as a coercion.

Equations

• Homeomorph.instCoeHomeomorphContinuousMap = { coe := Homeomorph.toContinuousMap }

@[simp]

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

@[simp]

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

@[simp]

theorem Homeomorph.symm_comp_toContinuousMap {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] (f : α ≃ₜ β) : ContinuousMap.comp (Homeomorph.toContinuousMap (Homeomorph.symm f)) (Homeomorph.toContinuousMap 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 : α ≃ₜ β) : ContinuousMap.comp (Homeomorph.toContinuousMap f) (Homeomorph.toContinuousMap (Homeomorph.symm f)) = ContinuousMap.id β

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