mathlib3 documentation

geometry.manifold.cont_mdiff_map

Smooth bundled map #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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

@[reducible]
def smooth_map {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type u_2} [normed_add_comm_group E] [normed_space 𝕜 E] {E' : Type u_3} [normed_add_comm_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
@[protected, instance]
def cont_mdiff_map.fun_like {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type u_2} [normed_add_comm_group E] [normed_space 𝕜 E] {E' : Type u_3} [normed_add_comm_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 : ℕ∞} :
fun_like (cont_mdiff_map I I' M M' n) M (λ (_x : M), M')
Equations
@[protected]
theorem cont_mdiff_map.cont_mdiff {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type u_2} [normed_add_comm_group E] [normed_space 𝕜 E] {E' : Type u_3} [normed_add_comm_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 : ℕ∞} (f : cont_mdiff_map I I' M M' n) :
cont_mdiff I I' n f
@[protected]
theorem cont_mdiff_map.smooth {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type u_2} [normed_add_comm_group E] [normed_space 𝕜 E] {E' : Type u_3} [normed_add_comm_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 : cont_mdiff_map I I' M M' ) :
smooth I I' f
@[protected, instance]
def cont_mdiff_map.continuous_map.has_coe {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type u_2} [normed_add_comm_group E] [normed_space 𝕜 E] {E' : Type u_3} [normed_add_comm_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 : ℕ∞} :
has_coe (cont_mdiff_map I I' M M' n) C(M, M')
Equations
@[simp]
theorem cont_mdiff_map.coe_fn_mk {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type u_2} [normed_add_comm_group E] [normed_space 𝕜 E] {E' : Type u_3} [normed_add_comm_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 : ℕ∞} (f : M M') (hf : cont_mdiff I I' n f) :
f, hf⟩ = f
theorem cont_mdiff_map.coe_inj {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type u_2} [normed_add_comm_group E] [normed_space 𝕜 E] {E' : Type u_3} [normed_add_comm_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 : ℕ∞} ⦃f g : cont_mdiff_map I I' M M' n⦄ (h : f = g) :
f = g
@[ext]
theorem cont_mdiff_map.ext {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type u_2} [normed_add_comm_group E] [normed_space 𝕜 E] {E' : Type u_3} [normed_add_comm_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 : ℕ∞} {f g : cont_mdiff_map I I' M M' n} (h : (x : M), f x = g x) :
f = g
@[protected, instance]
def cont_mdiff_map.continuous_map_class {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type u_2} [normed_add_comm_group E] [normed_space 𝕜 E] {E' : Type u_3} [normed_add_comm_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 : ℕ∞} :
Equations
def cont_mdiff_map.id {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type u_2} [normed_add_comm_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 : ℕ∞} :
cont_mdiff_map I I M M n

The identity as a smooth map.

Equations
def cont_mdiff_map.comp {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type u_2} [normed_add_comm_group E] [normed_space 𝕜 E] {E' : Type u_3} [normed_add_comm_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_add_comm_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 : ℕ∞} (f : cont_mdiff_map I' I'' M' M'' n) (g : cont_mdiff_map I I' M M' n) :
cont_mdiff_map I I'' M M'' n

The composition of smooth maps, as a smooth map.

Equations
@[simp]
theorem cont_mdiff_map.comp_apply {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type u_2} [normed_add_comm_group E] [normed_space 𝕜 E] {E' : Type u_3} [normed_add_comm_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_add_comm_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 : ℕ∞} (f : cont_mdiff_map I' I'' M' M'' n) (g : cont_mdiff_map I I' M M' n) (x : M) :
(f.comp g) x = f (g x)
@[protected, instance]
def cont_mdiff_map.inhabited {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type u_2} [normed_add_comm_group E] [normed_space 𝕜 E] {E' : Type u_3} [normed_add_comm_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 : ℕ∞} [inhabited M'] :
Equations
def cont_mdiff_map.const {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type u_2} [normed_add_comm_group E] [normed_space 𝕜 E] {E' : Type u_3} [normed_add_comm_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 : ℕ∞} (y : M') :
cont_mdiff_map I I' M M' n

Constant map as a smooth map

Equations
def cont_mdiff_map.fst {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type u_2} [normed_add_comm_group E] [normed_space 𝕜 E] {E' : Type u_3} [normed_add_comm_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 : ℕ∞} :
cont_mdiff_map (I.prod I') I (M × M') M n

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

Equations
def cont_mdiff_map.snd {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type u_2} [normed_add_comm_group E] [normed_space 𝕜 E] {E' : Type u_3} [normed_add_comm_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 : ℕ∞} :
cont_mdiff_map (I.prod I') I' (M × M') M' n

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

Equations
def cont_mdiff_map.prod_mk {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type u_2} [normed_add_comm_group E] [normed_space 𝕜 E] {E' : Type u_3} [normed_add_comm_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 : Type u_11} [normed_add_comm_group F] [normed_space 𝕜 F] {G : Type u_12} [topological_space G] {J : model_with_corners 𝕜 F G} {N : Type u_13} [topological_space N] [charted_space G N] {n : ℕ∞} (f : cont_mdiff_map J I N M n) (g : cont_mdiff_map J I' N M' n) :
cont_mdiff_map J (I.prod I') N (M × M') n

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

Equations
@[protected, instance]
Equations