Smooth bundled map

In this file we define the type ContMDiffMap of n times continuously differentiable bundled maps.

def ContMDiffMap {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {E' : Type u_3} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {H : Type u_4} [TopologicalSpace H] {H' : Type u_5} [TopologicalSpace H'] (I : ModelWithCorners 𝕜 E H) (I' : ModelWithCorners 𝕜 E' H') (M : Type u_6) [TopologicalSpace M] [ChartedSpace H M] (M' : Type u_7) [TopologicalSpace M'] [ChartedSpace H' M'] (n : ℕ∞) : Type (max 0 u_6 u_7)

Bundled n times continuously differentiable maps.

Equations

• ContMDiffMap I I' M M' n = { f : M → M' // ContMDiff I I' n f }

@[reducible]

def SmoothMap {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {E' : Type u_3} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {H : Type u_4} [TopologicalSpace H] {H' : Type u_5} [TopologicalSpace H'] (I : ModelWithCorners 𝕜 E H) (I' : ModelWithCorners 𝕜 E' H') (M : Type u_6) [TopologicalSpace M] [ChartedSpace H M] (M' : Type u_7) [TopologicalSpace M'] [ChartedSpace H' M'] : Type (max 0 u_6 u_7)

Bundled smooth maps.

Equations

• SmoothMap I I' M M' = ContMDiffMap I I' M M' ⊤

def Manifold.«termC^_⟮_,_;_,_⟯» : Lean.ParserDescr

Bundled n times continuously differentiable maps.

Equations

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

def Manifold.«termC^_⟮_,_;_⟯» : Lean.ParserDescr

Bundled n times continuously differentiable maps.

Equations

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

instance ContMDiffMap.instFunLike {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {E' : Type u_3} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {H : Type u_4} [TopologicalSpace H] {H' : Type u_5} [TopologicalSpace H'] {I : ModelWithCorners 𝕜 E H} {I' : ModelWithCorners 𝕜 E' H'} {M : Type u_6} [TopologicalSpace M] [ChartedSpace H M] {M' : Type u_7} [TopologicalSpace M'] [ChartedSpace H' M'] {n : ℕ∞} : FunLike (ContMDiffMap I I' M M' n) M M'

Equations

• ContMDiffMap.instFunLike = { coe := Subtype.val, coe_injective' := (_ : Function.Injective fun (a : { f : M → M' // ContMDiff I I' n f }) => ↑a) }

theorem ContMDiffMap.contMDiff {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {E' : Type u_3} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {H : Type u_4} [TopologicalSpace H] {H' : Type u_5} [TopologicalSpace H'] {I : ModelWithCorners 𝕜 E H} {I' : ModelWithCorners 𝕜 E' H'} {M : Type u_6} [TopologicalSpace M] [ChartedSpace H M] {M' : Type u_7} [TopologicalSpace M'] [ChartedSpace H' M'] {n : ℕ∞} (f : ContMDiffMap I I' M M' n) : ContMDiff I I' n ⇑f

theorem ContMDiffMap.smooth {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {E' : Type u_3} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {H : Type u_4} [TopologicalSpace H] {H' : Type u_5} [TopologicalSpace H'] {I : ModelWithCorners 𝕜 E H} {I' : ModelWithCorners 𝕜 E' H'} {M : Type u_6} [TopologicalSpace M] [ChartedSpace H M] {M' : Type u_7} [TopologicalSpace M'] [ChartedSpace H' M'] (f : ContMDiffMap I I' M M' ⊤) : Smooth I I' ⇑f

@[simp]

theorem ContMDiffMap.coeFn_mk {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {E' : Type u_3} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {H : Type u_4} [TopologicalSpace H] {H' : Type u_5} [TopologicalSpace H'] {I : ModelWithCorners 𝕜 E H} {I' : ModelWithCorners 𝕜 E' H'} {M : Type u_6} [TopologicalSpace M] [ChartedSpace H M] {M' : Type u_7} [TopologicalSpace M'] [ChartedSpace H' M'] {n : ℕ∞} (f : M → M') (hf : ContMDiff I I' n f) : ⇑{ val := f, property := hf } = f

theorem ContMDiffMap.coe_injective {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {E' : Type u_3} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {H : Type u_4} [TopologicalSpace H] {H' : Type u_5} [TopologicalSpace H'] {I : ModelWithCorners 𝕜 E H} {I' : ModelWithCorners 𝕜 E' H'} {M : Type u_6} [TopologicalSpace M] [ChartedSpace H M] {M' : Type u_7} [TopologicalSpace M'] [ChartedSpace H' M'] {n : ℕ∞} ⦃f : ContMDiffMap I I' M M' n⦄ ⦃g : ContMDiffMap I I' M M' n⦄ (h : ⇑f = ⇑g) : f = g

theorem ContMDiffMap.ext {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {E' : Type u_3} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {H : Type u_4} [TopologicalSpace H] {H' : Type u_5} [TopologicalSpace H'] {I : ModelWithCorners 𝕜 E H} {I' : ModelWithCorners 𝕜 E' H'} {M : Type u_6} [TopologicalSpace M] [ChartedSpace H M] {M' : Type u_7} [TopologicalSpace M'] [ChartedSpace H' M'] {n : ℕ∞} {f : ContMDiffMap I I' M M' n} {g : ContMDiffMap I I' M M' n} (h : ∀ (x : M), f x = g x) : f = g

instance ContMDiffMap.instContinuousMapClassContMDiffMapInstFunLike {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {E' : Type u_3} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {H : Type u_4} [TopologicalSpace H] {H' : Type u_5} [TopologicalSpace H'] {I : ModelWithCorners 𝕜 E H} {I' : ModelWithCorners 𝕜 E' H'} {M : Type u_6} [TopologicalSpace M] [ChartedSpace H M] {M' : Type u_7} [TopologicalSpace M'] [ChartedSpace H' M'] {n : ℕ∞} : ContinuousMapClass (ContMDiffMap I I' M M' n) M M'

Equations

• (_ : ContinuousMapClass (ContMDiffMap I I' M M' n) M M') = (_ : ContinuousMapClass (ContMDiffMap I I' M M' n) M M')

def ContMDiffMap.id {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_4} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_6} [TopologicalSpace M] [ChartedSpace H M] {n : ℕ∞} : ContMDiffMap I I M M n

The identity as a smooth map.

Equations

• ContMDiffMap.id = { val := id, property := (_ : ContMDiff I I n id) }

def ContMDiffMap.comp {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {E' : Type u_3} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {H : Type u_4} [TopologicalSpace H] {H' : Type u_5} [TopologicalSpace H'] {I : ModelWithCorners 𝕜 E H} {I' : ModelWithCorners 𝕜 E' H'} {M : Type u_6} [TopologicalSpace M] [ChartedSpace H M] {M' : Type u_7} [TopologicalSpace M'] [ChartedSpace H' M'] {E'' : Type u_8} [NormedAddCommGroup E''] [NormedSpace 𝕜 E''] {H'' : Type u_9} [TopologicalSpace H''] {I'' : ModelWithCorners 𝕜 E'' H''} {M'' : Type u_10} [TopologicalSpace M''] [ChartedSpace H'' M''] {n : ℕ∞} (f : ContMDiffMap I' I'' M' M'' n) (g : ContMDiffMap I I' M M' n) : ContMDiffMap I I'' M M'' n

The composition of smooth maps, as a smooth map.

Equations

• ContMDiffMap.comp f g = { val := fun (a : M) => f (g a), property := (_ : ContMDiff I I'' n (⇑f ∘ fun (a : M) => g a)) }

@[simp]

theorem ContMDiffMap.comp_apply {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {E' : Type u_3} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {H : Type u_4} [TopologicalSpace H] {H' : Type u_5} [TopologicalSpace H'] {I : ModelWithCorners 𝕜 E H} {I' : ModelWithCorners 𝕜 E' H'} {M : Type u_6} [TopologicalSpace M] [ChartedSpace H M] {M' : Type u_7} [TopologicalSpace M'] [ChartedSpace H' M'] {E'' : Type u_8} [NormedAddCommGroup E''] [NormedSpace 𝕜 E''] {H'' : Type u_9} [TopologicalSpace H''] {I'' : ModelWithCorners 𝕜 E'' H''} {M'' : Type u_10} [TopologicalSpace M''] [ChartedSpace H'' M''] {n : ℕ∞} (f : ContMDiffMap I' I'' M' M'' n) (g : ContMDiffMap I I' M M' n) (x : M) : (ContMDiffMap.comp f g) x = f (g x)

instance ContMDiffMap.instInhabitedContMDiffMap {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {E' : Type u_3} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {H : Type u_4} [TopologicalSpace H] {H' : Type u_5} [TopologicalSpace H'] {I : ModelWithCorners 𝕜 E H} {I' : ModelWithCorners 𝕜 E' H'} {M : Type u_6} [TopologicalSpace M] [ChartedSpace H M] {M' : Type u_7} [TopologicalSpace M'] [ChartedSpace H' M'] {n : ℕ∞} [Inhabited M'] : Inhabited (ContMDiffMap I I' M M' n)

Equations

• ContMDiffMap.instInhabitedContMDiffMap = { default := { val := fun (x : M) => default, property := (_ : ContMDiff I I' n fun (x : M) => default) } }

def ContMDiffMap.const {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {E' : Type u_3} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {H : Type u_4} [TopologicalSpace H] {H' : Type u_5} [TopologicalSpace H'] {I : ModelWithCorners 𝕜 E H} {I' : ModelWithCorners 𝕜 E' H'} {M : Type u_6} [TopologicalSpace M] [ChartedSpace H M] {M' : Type u_7} [TopologicalSpace M'] [ChartedSpace H' M'] {n : ℕ∞} (y : M') : ContMDiffMap I I' M M' n

Constant map as a smooth map

Equations

• ContMDiffMap.const y = { val := fun (x : M) => y, property := (_ : ContMDiff I I' n fun (x : M) => y) }

def ContMDiffMap.fst {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {E' : Type u_3} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {H : Type u_4} [TopologicalSpace H] {H' : Type u_5} [TopologicalSpace H'] {I : ModelWithCorners 𝕜 E H} {I' : ModelWithCorners 𝕜 E' H'} {M : Type u_6} [TopologicalSpace M] [ChartedSpace H M] {M' : Type u_7} [TopologicalSpace M'] [ChartedSpace H' M'] {n : ℕ∞} : ContMDiffMap (ModelWithCorners.prod I I') I (M × M') M n

The first projection of a product, as a smooth map.

Equations

• ContMDiffMap.fst = { val := Prod.fst, property := (_ : ContMDiff (ModelWithCorners.prod I I') I n Prod.fst) }

def ContMDiffMap.snd {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {E' : Type u_3} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {H : Type u_4} [TopologicalSpace H] {H' : Type u_5} [TopologicalSpace H'] {I : ModelWithCorners 𝕜 E H} {I' : ModelWithCorners 𝕜 E' H'} {M : Type u_6} [TopologicalSpace M] [ChartedSpace H M] {M' : Type u_7} [TopologicalSpace M'] [ChartedSpace H' M'] {n : ℕ∞} : ContMDiffMap (ModelWithCorners.prod I I') I' (M × M') M' n

The second projection of a product, as a smooth map.

Equations

• ContMDiffMap.snd = { val := Prod.snd, property := (_ : ContMDiff (ModelWithCorners.prod I I') I' n Prod.snd) }

def ContMDiffMap.prodMk {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {E' : Type u_3} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {H : Type u_4} [TopologicalSpace H] {H' : Type u_5} [TopologicalSpace H'] {I : ModelWithCorners 𝕜 E H} {I' : ModelWithCorners 𝕜 E' H'} {M : Type u_6} [TopologicalSpace M] [ChartedSpace H M] {M' : Type u_7} [TopologicalSpace M'] [ChartedSpace H' M'] {F : Type u_11} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {G : Type u_12} [TopologicalSpace G] {J : ModelWithCorners 𝕜 F G} {N : Type u_13} [TopologicalSpace N] [ChartedSpace G N] {n : ℕ∞} (f : ContMDiffMap J I N M n) (g : ContMDiffMap J I' N M' n) : ContMDiffMap J (ModelWithCorners.prod I I') N (M × M') n

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

Equations

• ContMDiffMap.prodMk f g = { val := fun (x : N) => (f x, g x), property := (_ : ContMDiff J (ModelWithCorners.prod I I') n fun (x : N) => (↑f x, g x)) }

instance ContinuousLinearMap.hasCoeToContMDiffMap {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {E' : Type u_3} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] (n : ℕ∞) : Coe (E →L[𝕜] E') (ContMDiffMap (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E') E E' n)

Equations

• ContinuousLinearMap.hasCoeToContMDiffMap n = { coe := fun (f : E →L[𝕜] E') => { val := ⇑f, property := (_ : ContMDiff (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E') n ⇑f) } }