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]
[smooth_manifold_with_corners I M]
(M' : Type u_7)
[topological_space M']
[charted_space H' M']
[smooth_manifold_with_corners I' M']
(n : with_top ℕ) :
Type (max u_6 u_7)
- to_fun : M → M'
- times_cont_mdiff_to_fun : times_cont_mdiff I I' n c.to_fun
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]
[smooth_manifold_with_corners I M]
(M' : Type u_7)
[topological_space M']
[charted_space H' M']
[smooth_manifold_with_corners I' M'] :
Type (max u_6 u_7)
Bundled smooth maps.
@[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]
[smooth_manifold_with_corners I M]
{M' : Type u_7}
[topological_space M']
[charted_space H' M']
[smooth_manifold_with_corners I' M']
{n : with_top ℕ} :
@[instance]
def
times_cont_mdiff_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]
[smooth_manifold_with_corners I M]
{M' : Type u_7}
[topological_space M']
[charted_space H' M']
[smooth_manifold_with_corners I' M']
{n : with_top ℕ} :
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]
[smooth_manifold_with_corners I M]
{M' : Type u_7}
[topological_space M']
[charted_space H' M']
[smooth_manifold_with_corners I' M']
{n : with_top ℕ}
(f : C^n⦃I, M; I', M'⦄) :
times_cont_mdiff I I' n ⇑f
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]
[smooth_manifold_with_corners I M]
{M' : Type u_7}
[topological_space M']
[charted_space H' M']
[smooth_manifold_with_corners I' M']
(f : C^⊤⦃I, M; I', 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]
[smooth_manifold_with_corners I M]
{M' : Type u_7}
[topological_space M']
[charted_space H' M']
[smooth_manifold_with_corners I' 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]
[smooth_manifold_with_corners I M]
{M' : Type u_7}
[topological_space M']
[charted_space H' M']
[smooth_manifold_with_corners I' 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]
[smooth_manifold_with_corners I M]
{n : with_top ℕ} :
The identity as a smooth map.
Equations
- times_cont_mdiff_map.id = {to_fun := id M, times_cont_mdiff_to_fun := _}
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]
[smooth_manifold_with_corners I M]
{M' : Type u_7}
[topological_space M']
[charted_space H' M']
[smooth_manifold_with_corners I' 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'']
[smooth_manifold_with_corners I'' M'']
{n : with_top ℕ}
(f : C^n⦃I', M'; I'', M''⦄)
(g : C^n⦃I, M; I', M'⦄) :
The composition of smooth maps, as a smooth map.
@[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]
[smooth_manifold_with_corners I M]
{M' : Type u_7}
[topological_space M']
[charted_space H' M']
[smooth_manifold_with_corners I' 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'']
[smooth_manifold_with_corners I'' M'']
{n : with_top ℕ}
(f : C^n⦃I', M'; I'', M''⦄)
(g : C^n⦃I, M; I', M'⦄)
(x : M) :
@[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]
[smooth_manifold_with_corners I M]
{M' : Type u_7}
[topological_space M']
[charted_space H' M']
[smooth_manifold_with_corners I' M']
{n : with_top ℕ}
[inhabited M'] :
Equations
- times_cont_mdiff_map.inhabited = {default := {to_fun := λ (_x : M), default M', times_cont_mdiff_to_fun := _}}
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]
[smooth_manifold_with_corners I M]
{M' : Type u_7}
[topological_space M']
[charted_space H' M']
[smooth_manifold_with_corners I' M']
{n : with_top ℕ}
(y : M') :
Constant map as a smooth map
Equations
- times_cont_mdiff_map.const y = {to_fun := λ (x : M), y, times_cont_mdiff_to_fun := _}
@[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 ℕ) :
Equations
- continuous_linear_map.has_coe_to_times_cont_mdiff_map n = {coe := λ (f : E →L[𝕜] E'), {to_fun := f.to_linear_map.to_fun, times_cont_mdiff_to_fun := _}}