# mathlibdocumentation

geometry.manifold.cont_mdiff_map

# Smooth bundled map #

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

structure cont_mdiff_map {𝕜 : Type u_1} {E : Type u_2} [ E] {E' : Type u_3} [ E'] {H : Type u_4} {H' : Type u_5} (I : H) (I' : H') (M : Type u_6) [ M] (M' : Type u_7) [ M'] (n : ℕ∞) :
Type (max u_6 u_7)
• to_fun : M → M'
• cont_mdiff_to_fun : I' n self.to_fun

Bundled n times continuously differentiable maps.

Instances for cont_mdiff_map
@[reducible]
def smooth_map {𝕜 : Type u_1} {E : Type u_2} [ E] {E' : Type u_3} [ E'] {H : Type u_4} {H' : Type u_5} (I : H) (I' : H') (M : Type u_6) [ M] (M' : Type u_7) [ M'] :
Type (max u_6 u_7)

Bundled smooth maps.

Equations
• I' M M' = I' M M'
@[protected, instance]
def cont_mdiff_map.has_coe_to_fun {𝕜 : Type u_1} {E : Type u_2} [ E] {E' : Type u_3} [ E'] {H : Type u_4} {H' : Type u_5} {I : H} {I' : H'} {M : Type u_6} [ M] {M' : Type u_7} [ M'] {n : ℕ∞} :
has_coe_to_fun I' M M' n) (λ (_x : I' M M' n), M → M')
Equations
@[protected, instance]
def cont_mdiff_map.continuous_map.has_coe {𝕜 : Type u_1} {E : Type u_2} [ E] {E' : Type u_3} [ E'] {H : Type u_4} {H' : Type u_5} {I : H} {I' : H'} {M : Type u_6} [ M] {M' : Type u_7} [ M'] {n : ℕ∞} :
has_coe I' M M' n) C(M, M')
Equations
@[simp]
theorem cont_mdiff_map.coe_fn_mk {𝕜 : Type u_1} {E : Type u_2} [ E] {E' : Type u_3} [ E'] {H : Type u_4} {H' : Type u_5} {I : H} {I' : H'} {M : Type u_6} [ M] {M' : Type u_7} [ M'] {n : ℕ∞} (f : M → M') (hf : I' n f) :
@[protected]
theorem cont_mdiff_map.cont_mdiff {𝕜 : Type u_1} {E : Type u_2} [ E] {E' : Type u_3} [ E'] {H : Type u_4} {H' : Type u_5} {I : H} {I' : H'} {M : Type u_6} [ M] {M' : Type u_7} [ M'] {n : ℕ∞} (f : I' M M' n) :
I' n f
@[protected]
theorem cont_mdiff_map.smooth {𝕜 : Type u_1} {E : Type u_2} [ E] {E' : Type u_3} [ E'] {H : Type u_4} {H' : Type u_5} {I : H} {I' : H'} {M : Type u_6} [ M] {M' : Type u_7} [ M'] (f : I' M M' ) :
I' f
@[protected]
theorem cont_mdiff_map.mdifferentiable' {𝕜 : Type u_1} {E : Type u_2} [ E] {E' : Type u_3} [ E'] {H : Type u_4} {H' : Type u_5} {I : H} {I' : H'} {M : Type u_6} [ M] {M' : Type u_7} [ M'] {n : ℕ∞} (f : I' M M' n) (hn : 1 n) :
I' f
@[protected]
theorem cont_mdiff_map.mdifferentiable {𝕜 : Type u_1} {E : Type u_2} [ E] {E' : Type u_3} [ E'] {H : Type u_4} {H' : Type u_5} {I : H} {I' : H'} {M : Type u_6} [ M] {M' : Type u_7} [ M'] (f : I' M M' ) :
I' f
@[protected]
theorem cont_mdiff_map.mdifferentiable_at {𝕜 : Type u_1} {E : Type u_2} [ E] {E' : Type u_3} [ E'] {H : Type u_4} {H' : Type u_5} {I : H} {I' : H'} {M : Type u_6} [ M] {M' : Type u_7} [ M'] (f : I' M M' ) {x : M} :
f x
theorem cont_mdiff_map.coe_inj {𝕜 : Type u_1} {E : Type u_2} [ E] {E' : Type u_3} [ E'] {H : Type u_4} {H' : Type u_5} {I : H} {I' : H'} {M : Type u_6} [ M] {M' : Type u_7} [ M'] {n : ℕ∞} ⦃f g : I' M M' n⦄ (h : f = g) :
f = g
@[ext]
theorem cont_mdiff_map.ext {𝕜 : Type u_1} {E : Type u_2} [ E] {E' : Type u_3} [ E'] {H : Type u_4} {H' : Type u_5} {I : H} {I' : H'} {M : Type u_6} [ M] {M' : Type u_7} [ M'] {n : ℕ∞} {f g : I' M M' n} (h : ∀ (x : M), f x = g x) :
f = g
def cont_mdiff_map.id {𝕜 : Type u_1} {E : Type u_2} [ E] {H : Type u_4} {I : H} {M : Type u_6} [ M] {n : ℕ∞} :
M M n

The identity as a smooth map.

Equations
def cont_mdiff_map.comp {𝕜 : Type u_1} {E : Type u_2} [ E] {E' : Type u_3} [ E'] {H : Type u_4} {H' : Type u_5} {I : H} {I' : H'} {M : Type u_6} [ M] {M' : Type u_7} [ M'] {E'' : Type u_8} [ E''] {H'' : Type u_9} [topological_space H''] {I'' : E'' H''} {M'' : Type u_10} [topological_space M''] [ M''] {n : ℕ∞} (f : I'' M' M'' n) (g : I' M M' n) :
I'' M M'' n

The composition of smooth maps, as a smooth map.

Equations
@[simp]
theorem cont_mdiff_map.comp_apply {𝕜 : Type u_1} {E : Type u_2} [ E] {E' : Type u_3} [ E'] {H : Type u_4} {H' : Type u_5} {I : H} {I' : H'} {M : Type u_6} [ M] {M' : Type u_7} [ M'] {E'' : Type u_8} [ E''] {H'' : Type u_9} [topological_space H''] {I'' : E'' H''} {M'' : Type u_10} [topological_space M''] [ M''] {n : ℕ∞} (f : I'' M' M'' n) (g : I' M M' n) (x : M) :
(f.comp g) x = f (g x)
@[protected, instance]
def cont_mdiff_map.inhabited {𝕜 : Type u_1} {E : Type u_2} [ E] {E' : Type u_3} [ E'] {H : Type u_4} {H' : Type u_5} {I : H} {I' : H'} {M : Type u_6} [ M] {M' : Type u_7} [ M'] {n : ℕ∞} [inhabited M'] :
inhabited I' M M' n)
Equations
def cont_mdiff_map.const {𝕜 : Type u_1} {E : Type u_2} [ E] {E' : Type u_3} [ E'] {H : Type u_4} {H' : Type u_5} {I : H} {I' : H'} {M : Type u_6} [ M] {M' : Type u_7} [ M'] {n : ℕ∞} (y : M') :
I' M M' n

Constant map as a smooth map

Equations
@[protected, instance]
def continuous_linear_map.has_coe_to_cont_mdiff_map {𝕜 : Type u_1} {E : Type u_2} [ E] {E' : Type u_3} [ E'] (n : ℕ∞) :
has_coe (E →L[𝕜] E') E') E E' n)
Equations