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)
- 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]
(M' : Type u_7)
[topological_space M']
[charted_space H' M'] :
Type (max u_6 u_7)
Bundled smooth maps.
@[protected, 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 ℕ} :
@[protected, 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 ℕ} :
@[protected]
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'⟯) :
times_cont_mdiff I I' n ⇑f
@[protected]
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'⟯) :
@[protected]
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) :
mdifferentiable I I' ⇑f
@[protected]
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'⟯) :
mdifferentiable I I' ⇑f
@[protected]
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} :
mdifferentiable_at I I' ⇑f x
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
- 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]
{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'⟯) :
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]
{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) :
@[protected, 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
- 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]
{M' : Type u_7}
[topological_space M']
[charted_space H' 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 := _}
@[protected, 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 := _}}