mathlib documentation

geometry.manifold.times_cont_mdiff_map

Smooth bundled map #

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

structure times_cont_mdiff_map {𝕜 : Type u_1} [nondiscrete_normed_field 𝕜] {E : Type u_2} [normed_group E] [normed_space 𝕜 E] {E' : Type u_3} [normed_group E'] [normed_space 𝕜 E'] {H : Type u_4} [topological_space H] {H' : Type u_5} [topological_space H'] (I : model_with_corners 𝕜 E H) (I' : model_with_corners 𝕜 E' H') (M : Type u_6) [topological_space M] [charted_space H M] (M' : Type u_7) [topological_space M'] [charted_space H' M'] (n : with_top ℕ) :
Type (max u_6 u_7)

Bundled n times continuously differentiable maps.

def smooth_map {𝕜 : Type u_1} [nondiscrete_normed_field 𝕜] {E : Type u_2} [normed_group E] [normed_space 𝕜 E] {E' : Type u_3} [normed_group E'] [normed_space 𝕜 E'] {H : Type u_4} [topological_space H] {H' : Type u_5} [topological_space H'] (I : model_with_corners 𝕜 E H) (I' : model_with_corners 𝕜 E' H') (M : Type u_6) [topological_space M] [charted_space H M] (M' : Type u_7) [topological_space M'] [charted_space H' M'] :
Type (max u_6 u_7)

Bundled smooth maps.

Equations
@[instance]
def times_cont_mdiff_map.has_coe_to_fun {𝕜 : Type u_1} [nondiscrete_normed_field 𝕜] {E : Type u_2} [normed_group E] [normed_space 𝕜 E] {E' : Type u_3} [normed_group E'] [normed_space 𝕜 E'] {H : Type u_4} [topological_space H] {H' : Type u_5} [topological_space H'] {I : model_with_corners 𝕜 E H} {I' : model_with_corners 𝕜 E' H'} {M : Type u_6} [topological_space M] [charted_space H M] {M' : Type u_7} [topological_space M'] [charted_space H' M'] {n : with_top ℕ} :
has_coe_to_fun C^n⟮I, M; I', M'⟯ (λ (_x : C^n⟮I, M; I', M'⟯), M → M')
Equations
@[instance]
def times_cont_mdiff_map.continuous_map.has_coe {𝕜 : Type u_1} [nondiscrete_normed_field 𝕜] {E : Type u_2} [normed_group E] [normed_space 𝕜 E] {E' : Type u_3} [normed_group E'] [normed_space 𝕜 E'] {H : Type u_4} [topological_space H] {H' : Type u_5} [topological_space H'] {I : model_with_corners 𝕜 E H} {I' : model_with_corners 𝕜 E' H'} {M : Type u_6} [topological_space M] [charted_space H M] {M' : Type u_7} [topological_space M'] [charted_space H' M'] {n : with_top ℕ} :
Equations
@[simp]
theorem times_cont_mdiff_map.coe_fn_mk {𝕜 : Type u_1} [nondiscrete_normed_field 𝕜] {E : Type u_2} [normed_group E] [normed_space 𝕜 E] {E' : Type u_3} [normed_group E'] [normed_space 𝕜 E'] {H : Type u_4} [topological_space H] {H' : Type u_5} [topological_space H'] {I : model_with_corners 𝕜 E H} {I' : model_with_corners 𝕜 E' H'} {M : Type u_6} [topological_space M] [charted_space H M] {M' : Type u_7} [topological_space M'] [charted_space H' M'] {n : with_top ℕ} (f : M → M') (hf : times_cont_mdiff I I' n f) :
theorem times_cont_mdiff_map.times_cont_mdiff {𝕜 : Type u_1} [nondiscrete_normed_field 𝕜] {E : Type u_2} [normed_group E] [normed_space 𝕜 E] {E' : Type u_3} [normed_group E'] [normed_space 𝕜 E'] {H : Type u_4} [topological_space H] {H' : Type u_5} [topological_space H'] {I : model_with_corners 𝕜 E H} {I' : model_with_corners 𝕜 E' H'} {M : Type u_6} [topological_space M] [charted_space H M] {M' : Type u_7} [topological_space M'] [charted_space H' M'] {n : with_top ℕ} (f : C^n⟮I, M; I', M'⟯) :
theorem times_cont_mdiff_map.smooth {𝕜 : Type u_1} [nondiscrete_normed_field 𝕜] {E : Type u_2} [normed_group E] [normed_space 𝕜 E] {E' : Type u_3} [normed_group E'] [normed_space 𝕜 E'] {H : Type u_4} [topological_space H] {H' : Type u_5} [topological_space H'] {I : model_with_corners 𝕜 E H} {I' : model_with_corners 𝕜 E' H'} {M : Type u_6} [topological_space M] [charted_space H M] {M' : Type u_7} [topological_space M'] [charted_space H' M'] (f : C^⊤⟮I, M; I', M'⟯) :
theorem times_cont_mdiff_map.mdifferentiable' {𝕜 : Type u_1} [nondiscrete_normed_field 𝕜] {E : Type u_2} [normed_group E] [normed_space 𝕜 E] {E' : Type u_3} [normed_group E'] [normed_space 𝕜 E'] {H : Type u_4} [topological_space H] {H' : Type u_5} [topological_space H'] {I : model_with_corners 𝕜 E H} {I' : model_with_corners 𝕜 E' H'} {M : Type u_6} [topological_space M] [charted_space H M] {M' : Type u_7} [topological_space M'] [charted_space H' M'] {n : with_top ℕ} (f : C^n⟮I, M; I', M'⟯) (hn : 1 ≤ n) :
theorem times_cont_mdiff_map.mdifferentiable {𝕜 : Type u_1} [nondiscrete_normed_field 𝕜] {E : Type u_2} [normed_group E] [normed_space 𝕜 E] {E' : Type u_3} [normed_group E'] [normed_space 𝕜 E'] {H : Type u_4} [topological_space H] {H' : Type u_5} [topological_space H'] {I : model_with_corners 𝕜 E H} {I' : model_with_corners 𝕜 E' H'} {M : Type u_6} [topological_space M] [charted_space H M] {M' : Type u_7} [topological_space M'] [charted_space H' M'] (f : C^⊤⟮I, M; I', M'⟯) :
theorem times_cont_mdiff_map.mdifferentiable_at {𝕜 : Type u_1} [nondiscrete_normed_field 𝕜] {E : Type u_2} [normed_group E] [normed_space 𝕜 E] {E' : Type u_3} [normed_group E'] [normed_space 𝕜 E'] {H : Type u_4} [topological_space H] {H' : Type u_5} [topological_space H'] {I : model_with_corners 𝕜 E H} {I' : model_with_corners 𝕜 E' H'} {M : Type u_6} [topological_space M] [charted_space H M] {M' : Type u_7} [topological_space M'] [charted_space H' M'] (f : C^⊤⟮I, M; I', M'⟯) {x : M} :
theorem times_cont_mdiff_map.coe_inj {𝕜 : Type u_1} [nondiscrete_normed_field 𝕜] {E : Type u_2} [normed_group E] [normed_space 𝕜 E] {E' : Type u_3} [normed_group E'] [normed_space 𝕜 E'] {H : Type u_4} [topological_space H] {H' : Type u_5} [topological_space H'] {I : model_with_corners 𝕜 E H} {I' : model_with_corners 𝕜 E' H'} {M : Type u_6} [topological_space M] [charted_space H M] {M' : Type u_7} [topological_space M'] [charted_space H' M'] {n : with_top ℕ} ⌃f g : C^n⟮I, M; I', M'⟯⦄ (h : ⇑f = ⇑g) :
f = g
@[ext]
theorem times_cont_mdiff_map.ext {𝕜 : Type u_1} [nondiscrete_normed_field 𝕜] {E : Type u_2} [normed_group E] [normed_space 𝕜 E] {E' : Type u_3} [normed_group E'] [normed_space 𝕜 E'] {H : Type u_4} [topological_space H] {H' : Type u_5} [topological_space H'] {I : model_with_corners 𝕜 E H} {I' : model_with_corners 𝕜 E' H'} {M : Type u_6} [topological_space M] [charted_space H M] {M' : Type u_7} [topological_space M'] [charted_space H' M'] {n : with_top ℕ} {f g : C^n⟮I, M; I', M'⟯} (h : ∀ (x : M), ⇑f x = ⇑g x) :
f = g
def times_cont_mdiff_map.id {𝕜 : Type u_1} [nondiscrete_normed_field 𝕜] {E : Type u_2} [normed_group E] [normed_space 𝕜 E] {H : Type u_4} [topological_space H] {I : model_with_corners 𝕜 E H} {M : Type u_6} [topological_space M] [charted_space H M] {n : with_top ℕ} :

The identity as a smooth map.

Equations
def times_cont_mdiff_map.comp {𝕜 : Type u_1} [nondiscrete_normed_field 𝕜] {E : Type u_2} [normed_group E] [normed_space 𝕜 E] {E' : Type u_3} [normed_group E'] [normed_space 𝕜 E'] {H : Type u_4} [topological_space H] {H' : Type u_5} [topological_space H'] {I : model_with_corners 𝕜 E H} {I' : model_with_corners 𝕜 E' H'} {M : Type u_6} [topological_space M] [charted_space H M] {M' : Type u_7} [topological_space M'] [charted_space H' M'] {E'' : Type u_8} [normed_group E''] [normed_space 𝕜 E''] {H'' : Type u_9} [topological_space H''] {I'' : model_with_corners 𝕜 E'' H''} {M'' : Type u_10} [topological_space M''] [charted_space H'' M''] {n : with_top ℕ} (f : C^n⟮I', M'; I'', M''⟯) (g : C^n⟮I, M; I', M'⟯) :
C^n⟮I, M; I'', M''⟯

The composition of smooth maps, as a smooth map.

Equations
@[simp]
theorem times_cont_mdiff_map.comp_apply {𝕜 : Type u_1} [nondiscrete_normed_field 𝕜] {E : Type u_2} [normed_group E] [normed_space 𝕜 E] {E' : Type u_3} [normed_group E'] [normed_space 𝕜 E'] {H : Type u_4} [topological_space H] {H' : Type u_5} [topological_space H'] {I : model_with_corners 𝕜 E H} {I' : model_with_corners 𝕜 E' H'} {M : Type u_6} [topological_space M] [charted_space H M] {M' : Type u_7} [topological_space M'] [charted_space H' M'] {E'' : Type u_8} [normed_group E''] [normed_space 𝕜 E''] {H'' : Type u_9} [topological_space H''] {I'' : model_with_corners 𝕜 E'' H''} {M'' : Type u_10} [topological_space M''] [charted_space H'' M''] {n : with_top ℕ} (f : C^n⟮I', M'; I'', M''⟯) (g : C^n⟮I, M; I', M'⟯) (x : M) :
⇑(f.comp g) x = ⇑f (⇑g x)
@[instance]
def times_cont_mdiff_map.inhabited {𝕜 : Type u_1} [nondiscrete_normed_field 𝕜] {E : Type u_2} [normed_group E] [normed_space 𝕜 E] {E' : Type u_3} [normed_group E'] [normed_space 𝕜 E'] {H : Type u_4} [topological_space H] {H' : Type u_5} [topological_space H'] {I : model_with_corners 𝕜 E H} {I' : model_with_corners 𝕜 E' H'} {M : Type u_6} [topological_space M] [charted_space H M] {M' : Type u_7} [topological_space M'] [charted_space H' M'] {n : with_top ℕ} [inhabited M'] :
Equations
def times_cont_mdiff_map.const {𝕜 : Type u_1} [nondiscrete_normed_field 𝕜] {E : Type u_2} [normed_group E] [normed_space 𝕜 E] {E' : Type u_3} [normed_group E'] [normed_space 𝕜 E'] {H : Type u_4} [topological_space H] {H' : Type u_5} [topological_space H'] {I : model_with_corners 𝕜 E H} {I' : model_with_corners 𝕜 E' H'} {M : Type u_6} [topological_space M] [charted_space H M] {M' : Type u_7} [topological_space M'] [charted_space H' M'] {n : with_top ℕ} (y : M') :

Constant map as a smooth map

Equations
@[instance]
def continuous_linear_map.has_coe_to_times_cont_mdiff_map {𝕜 : Type u_1} [nondiscrete_normed_field 𝕜] {E : Type u_2} [normed_group E] [normed_space 𝕜 E] {E' : Type u_3} [normed_group E'] [normed_space 𝕜 E'] (n : with_top ℕ) :
has_coe (E →L[𝕜] E') C^n⟮𝓘(𝕜, E), E; 𝓘(𝕜, E'), E'⟯
Equations