Smooth sections #
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_section of n times continuously differentiable
sections of a smooth vector bundle over a manifold M and prove that it's a module.
structure
cont_mdiff_section
{𝕜 : 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]
[smooth_manifold_with_corners I M]
(F : Type u_11)
[normed_add_comm_group F]
[normed_space 𝕜 F]
(n : ℕ∞)
(V : M → Type u_12)
[topological_space (bundle.total_space F V)]
[Π (x : M), add_comm_group (V x)]
[Π (x : M), module 𝕜 (V x)]
[Π (x : M), topological_space (V x)]
[fiber_bundle F V]
[vector_bundle 𝕜 F V]
[smooth_vector_bundle F V I] :
Type (max u_12 u_6)
- to_fun : Π (x : M), V x
- cont_mdiff_to_fun : cont_mdiff I (I.prod (model_with_corners_self 𝕜 F)) n (λ (x : M), {proj := x, snd := self.to_fun x})
Bundled n times continuously differentiable sections of a vector bundle.
Instances for cont_mdiff_section
- cont_mdiff_section.has_sizeof_inst
- cont_mdiff_section.has_coe_to_fun
- cont_mdiff_section.has_add
- cont_mdiff_section.has_sub
- cont_mdiff_section.has_zero
- cont_mdiff_section.inhabited
- cont_mdiff_section.has_smul
- cont_mdiff_section.has_neg
- cont_mdiff_section.has_nsmul
- cont_mdiff_section.has_zsmul
- cont_mdiff_section.add_comm_group
- cont_mdiff_section.module
@[reducible]
def
smooth_section
{𝕜 : 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]
[smooth_manifold_with_corners I M]
(F : Type u_11)
[normed_add_comm_group F]
[normed_space 𝕜 F]
(V : M → Type u_12)
[topological_space (bundle.total_space F V)]
[Π (x : M), add_comm_group (V x)]
[Π (x : M), module 𝕜 (V x)]
[Π (x : M), topological_space (V x)]
[fiber_bundle F V]
[vector_bundle 𝕜 F V]
[smooth_vector_bundle F V I] :
Type (max u_12 u_6)
Bundled smooth sections of a vector bundle.
Equations
- smooth_section I F V = cont_mdiff_section I F ⊤ V
@[protected, instance]
def
cont_mdiff_section.has_coe_to_fun
{𝕜 : 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]
[smooth_manifold_with_corners I M]
{F : Type u_11}
[normed_add_comm_group F]
[normed_space 𝕜 F]
{n : ℕ∞}
{V : M → Type u_12}
[topological_space (bundle.total_space F V)]
[Π (x : M), add_comm_group (V x)]
[Π (x : M), module 𝕜 (V x)]
[Π (x : M), topological_space (V x)]
[fiber_bundle F V]
[vector_bundle 𝕜 F V]
[smooth_vector_bundle F V I] :
has_coe_to_fun (cont_mdiff_section I F n V) (λ (s : cont_mdiff_section I F n V), Π (x : M), V x)
Equations
- cont_mdiff_section.has_coe_to_fun = {coe := cont_mdiff_section.to_fun _inst_26}
@[simp]
theorem
cont_mdiff_section.coe_fn_mk
{𝕜 : 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]
[smooth_manifold_with_corners I M]
{F : Type u_11}
[normed_add_comm_group F]
[normed_space 𝕜 F]
{n : ℕ∞}
{V : M → Type u_12}
[topological_space (bundle.total_space F V)]
[Π (x : M), add_comm_group (V x)]
[Π (x : M), module 𝕜 (V x)]
[Π (x : M), topological_space (V x)]
[fiber_bundle F V]
[vector_bundle 𝕜 F V]
[smooth_vector_bundle F V I]
(s : Π (x : M), V x)
(hs : cont_mdiff I (I.prod (model_with_corners_self 𝕜 F)) n (λ (x : M), {proj := x, snd := s x})) :
⇑{to_fun := s, cont_mdiff_to_fun := hs} = s
@[protected]
theorem
cont_mdiff_section.cont_mdiff
{𝕜 : 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]
[smooth_manifold_with_corners I M]
{F : Type u_11}
[normed_add_comm_group F]
[normed_space 𝕜 F]
{n : ℕ∞}
{V : M → Type u_12}
[topological_space (bundle.total_space F V)]
[Π (x : M), add_comm_group (V x)]
[Π (x : M), module 𝕜 (V x)]
[Π (x : M), topological_space (V x)]
[fiber_bundle F V]
[vector_bundle 𝕜 F V]
[smooth_vector_bundle F V I]
(s : cont_mdiff_section I F n V) :
cont_mdiff I (I.prod (model_with_corners_self 𝕜 F)) n (λ (x : M), {proj := x, snd := ⇑s x})
@[protected]
theorem
cont_mdiff_section.smooth
{𝕜 : 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]
[smooth_manifold_with_corners I M]
{F : Type u_11}
[normed_add_comm_group F]
[normed_space 𝕜 F]
{V : M → Type u_12}
[topological_space (bundle.total_space F V)]
[Π (x : M), add_comm_group (V x)]
[Π (x : M), module 𝕜 (V x)]
[Π (x : M), topological_space (V x)]
[fiber_bundle F V]
[vector_bundle 𝕜 F V]
[smooth_vector_bundle F V I]
(s : cont_mdiff_section I F ⊤ V) :
@[protected]
theorem
cont_mdiff_section.mdifferentiable'
{𝕜 : 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]
[smooth_manifold_with_corners I M]
{F : Type u_11}
[normed_add_comm_group F]
[normed_space 𝕜 F]
{n : ℕ∞}
{V : M → Type u_12}
[topological_space (bundle.total_space F V)]
[Π (x : M), add_comm_group (V x)]
[Π (x : M), module 𝕜 (V x)]
[Π (x : M), topological_space (V x)]
[fiber_bundle F V]
[vector_bundle 𝕜 F V]
[smooth_vector_bundle F V I]
(s : cont_mdiff_section I F n V)
(hn : 1 ≤ n) :
mdifferentiable I (I.prod (model_with_corners_self 𝕜 F)) (λ (x : M), {proj := x, snd := ⇑s x})
@[protected]
theorem
cont_mdiff_section.mdifferentiable
{𝕜 : 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]
[smooth_manifold_with_corners I M]
{F : Type u_11}
[normed_add_comm_group F]
[normed_space 𝕜 F]
{V : M → Type u_12}
[topological_space (bundle.total_space F V)]
[Π (x : M), add_comm_group (V x)]
[Π (x : M), module 𝕜 (V x)]
[Π (x : M), topological_space (V x)]
[fiber_bundle F V]
[vector_bundle 𝕜 F V]
[smooth_vector_bundle F V I]
(s : cont_mdiff_section I F ⊤ V) :
mdifferentiable I (I.prod (model_with_corners_self 𝕜 F)) (λ (x : M), {proj := x, snd := ⇑s x})
@[protected]
theorem
cont_mdiff_section.mdifferentiable_at
{𝕜 : 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]
[smooth_manifold_with_corners I M]
{F : Type u_11}
[normed_add_comm_group F]
[normed_space 𝕜 F]
{V : M → Type u_12}
[topological_space (bundle.total_space F V)]
[Π (x : M), add_comm_group (V x)]
[Π (x : M), module 𝕜 (V x)]
[Π (x : M), topological_space (V x)]
[fiber_bundle F V]
[vector_bundle 𝕜 F V]
[smooth_vector_bundle F V I]
(s : cont_mdiff_section I F ⊤ V)
{x : M} :
mdifferentiable_at I (I.prod (model_with_corners_self 𝕜 F)) (λ (x : M), {proj := x, snd := ⇑s x}) x
theorem
cont_mdiff_section.coe_inj
{𝕜 : 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]
[smooth_manifold_with_corners I M]
{F : Type u_11}
[normed_add_comm_group F]
[normed_space 𝕜 F]
{n : ℕ∞}
{V : M → Type u_12}
[topological_space (bundle.total_space F V)]
[Π (x : M), add_comm_group (V x)]
[Π (x : M), module 𝕜 (V x)]
[Π (x : M), topological_space (V x)]
[fiber_bundle F V]
[vector_bundle 𝕜 F V]
[smooth_vector_bundle F V I]
⦃s t : cont_mdiff_section I F n V⦄
(h : ⇑s = ⇑t) :
s = t
theorem
cont_mdiff_section.coe_injective
{𝕜 : 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]
[smooth_manifold_with_corners I M]
{F : Type u_11}
[normed_add_comm_group F]
[normed_space 𝕜 F]
{n : ℕ∞}
{V : M → Type u_12}
[topological_space (bundle.total_space F V)]
[Π (x : M), add_comm_group (V x)]
[Π (x : M), module 𝕜 (V x)]
[Π (x : M), topological_space (V x)]
[fiber_bundle F V]
[vector_bundle 𝕜 F V]
[smooth_vector_bundle F V I] :
@[ext]
theorem
cont_mdiff_section.ext
{𝕜 : 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]
[smooth_manifold_with_corners I M]
{F : Type u_11}
[normed_add_comm_group F]
[normed_space 𝕜 F]
{n : ℕ∞}
{V : M → Type u_12}
[topological_space (bundle.total_space F V)]
[Π (x : M), add_comm_group (V x)]
[Π (x : M), module 𝕜 (V x)]
[Π (x : M), topological_space (V x)]
[fiber_bundle F V]
[vector_bundle 𝕜 F V]
[smooth_vector_bundle F V I]
{s t : cont_mdiff_section I F n V}
(h : ∀ (x : M), ⇑s x = ⇑t x) :
s = t
@[protected, instance]
def
cont_mdiff_section.has_add
{𝕜 : 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]
[smooth_manifold_with_corners I M]
{F : Type u_11}
[normed_add_comm_group F]
[normed_space 𝕜 F]
{n : ℕ∞}
{V : M → Type u_12}
[topological_space (bundle.total_space F V)]
[Π (x : M), add_comm_group (V x)]
[Π (x : M), module 𝕜 (V x)]
[Π (x : M), topological_space (V x)]
[fiber_bundle F V]
[vector_bundle 𝕜 F V]
[smooth_vector_bundle F V I] :
has_add (cont_mdiff_section I F n V)
Equations
- cont_mdiff_section.has_add = {add := λ (s t : cont_mdiff_section I F n V), {to_fun := ⇑s + ⇑t, cont_mdiff_to_fun := _}}
@[simp]
theorem
cont_mdiff_section.coe_add
{𝕜 : 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]
[smooth_manifold_with_corners I M]
{F : Type u_11}
[normed_add_comm_group F]
[normed_space 𝕜 F]
{n : ℕ∞}
{V : M → Type u_12}
[topological_space (bundle.total_space F V)]
[Π (x : M), add_comm_group (V x)]
[Π (x : M), module 𝕜 (V x)]
[Π (x : M), topological_space (V x)]
[fiber_bundle F V]
[vector_bundle 𝕜 F V]
[smooth_vector_bundle F V I]
(s t : cont_mdiff_section I F n V) :
@[protected, instance]
def
cont_mdiff_section.has_sub
{𝕜 : 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]
[smooth_manifold_with_corners I M]
{F : Type u_11}
[normed_add_comm_group F]
[normed_space 𝕜 F]
{n : ℕ∞}
{V : M → Type u_12}
[topological_space (bundle.total_space F V)]
[Π (x : M), add_comm_group (V x)]
[Π (x : M), module 𝕜 (V x)]
[Π (x : M), topological_space (V x)]
[fiber_bundle F V]
[vector_bundle 𝕜 F V]
[smooth_vector_bundle F V I] :
has_sub (cont_mdiff_section I F n V)
Equations
- cont_mdiff_section.has_sub = {sub := λ (s t : cont_mdiff_section I F n V), {to_fun := ⇑s - ⇑t, cont_mdiff_to_fun := _}}
@[simp]
theorem
cont_mdiff_section.coe_sub
{𝕜 : 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]
[smooth_manifold_with_corners I M]
{F : Type u_11}
[normed_add_comm_group F]
[normed_space 𝕜 F]
{n : ℕ∞}
{V : M → Type u_12}
[topological_space (bundle.total_space F V)]
[Π (x : M), add_comm_group (V x)]
[Π (x : M), module 𝕜 (V x)]
[Π (x : M), topological_space (V x)]
[fiber_bundle F V]
[vector_bundle 𝕜 F V]
[smooth_vector_bundle F V I]
(s t : cont_mdiff_section I F n V) :
@[protected, instance]
def
cont_mdiff_section.has_zero
{𝕜 : 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]
[smooth_manifold_with_corners I M]
{F : Type u_11}
[normed_add_comm_group F]
[normed_space 𝕜 F]
{n : ℕ∞}
{V : M → Type u_12}
[topological_space (bundle.total_space F V)]
[Π (x : M), add_comm_group (V x)]
[Π (x : M), module 𝕜 (V x)]
[Π (x : M), topological_space (V x)]
[fiber_bundle F V]
[vector_bundle 𝕜 F V]
[smooth_vector_bundle F V I] :
has_zero (cont_mdiff_section I F n V)
Equations
- cont_mdiff_section.has_zero = {zero := {to_fun := λ (x : M), 0, cont_mdiff_to_fun := _}}
@[protected, instance]
def
cont_mdiff_section.inhabited
{𝕜 : 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]
[smooth_manifold_with_corners I M]
{F : Type u_11}
[normed_add_comm_group F]
[normed_space 𝕜 F]
{n : ℕ∞}
{V : M → Type u_12}
[topological_space (bundle.total_space F V)]
[Π (x : M), add_comm_group (V x)]
[Π (x : M), module 𝕜 (V x)]
[Π (x : M), topological_space (V x)]
[fiber_bundle F V]
[vector_bundle 𝕜 F V]
[smooth_vector_bundle F V I] :
inhabited (cont_mdiff_section I F n V)
Equations
@[simp]
theorem
cont_mdiff_section.coe_zero
{𝕜 : 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]
[smooth_manifold_with_corners I M]
{F : Type u_11}
[normed_add_comm_group F]
[normed_space 𝕜 F]
{n : ℕ∞}
{V : M → Type u_12}
[topological_space (bundle.total_space F V)]
[Π (x : M), add_comm_group (V x)]
[Π (x : M), module 𝕜 (V x)]
[Π (x : M), topological_space (V x)]
[fiber_bundle F V]
[vector_bundle 𝕜 F V]
[smooth_vector_bundle F V I] :
@[protected, instance]
def
cont_mdiff_section.has_smul
{𝕜 : 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]
[smooth_manifold_with_corners I M]
{F : Type u_11}
[normed_add_comm_group F]
[normed_space 𝕜 F]
{n : ℕ∞}
{V : M → Type u_12}
[topological_space (bundle.total_space F V)]
[Π (x : M), add_comm_group (V x)]
[Π (x : M), module 𝕜 (V x)]
[Π (x : M), topological_space (V x)]
[fiber_bundle F V]
[vector_bundle 𝕜 F V]
[smooth_vector_bundle F V I] :
has_smul 𝕜 (cont_mdiff_section I F n V)
Equations
- cont_mdiff_section.has_smul = {smul := λ (c : 𝕜) (s : cont_mdiff_section I F n V), {to_fun := c • ⇑s, cont_mdiff_to_fun := _}}
@[simp]
theorem
cont_mdiff_section.coe_smul
{𝕜 : 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]
[smooth_manifold_with_corners I M]
{F : Type u_11}
[normed_add_comm_group F]
[normed_space 𝕜 F]
{n : ℕ∞}
{V : M → Type u_12}
[topological_space (bundle.total_space F V)]
[Π (x : M), add_comm_group (V x)]
[Π (x : M), module 𝕜 (V x)]
[Π (x : M), topological_space (V x)]
[fiber_bundle F V]
[vector_bundle 𝕜 F V]
[smooth_vector_bundle F V I]
(r : 𝕜)
(s : cont_mdiff_section I F n V) :
@[protected, instance]
def
cont_mdiff_section.has_neg
{𝕜 : 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]
[smooth_manifold_with_corners I M]
{F : Type u_11}
[normed_add_comm_group F]
[normed_space 𝕜 F]
{n : ℕ∞}
{V : M → Type u_12}
[topological_space (bundle.total_space F V)]
[Π (x : M), add_comm_group (V x)]
[Π (x : M), module 𝕜 (V x)]
[Π (x : M), topological_space (V x)]
[fiber_bundle F V]
[vector_bundle 𝕜 F V]
[smooth_vector_bundle F V I] :
has_neg (cont_mdiff_section I F n V)
Equations
- cont_mdiff_section.has_neg = {neg := λ (s : cont_mdiff_section I F n V), {to_fun := -⇑s, cont_mdiff_to_fun := _}}
@[simp]
theorem
cont_mdiff_section.coe_neg
{𝕜 : 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]
[smooth_manifold_with_corners I M]
{F : Type u_11}
[normed_add_comm_group F]
[normed_space 𝕜 F]
{n : ℕ∞}
{V : M → Type u_12}
[topological_space (bundle.total_space F V)]
[Π (x : M), add_comm_group (V x)]
[Π (x : M), module 𝕜 (V x)]
[Π (x : M), topological_space (V x)]
[fiber_bundle F V]
[vector_bundle 𝕜 F V]
[smooth_vector_bundle F V I]
(s : cont_mdiff_section I F n V) :
@[protected, instance]
def
cont_mdiff_section.has_nsmul
{𝕜 : 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]
[smooth_manifold_with_corners I M]
{F : Type u_11}
[normed_add_comm_group F]
[normed_space 𝕜 F]
{n : ℕ∞}
{V : M → Type u_12}
[topological_space (bundle.total_space F V)]
[Π (x : M), add_comm_group (V x)]
[Π (x : M), module 𝕜 (V x)]
[Π (x : M), topological_space (V x)]
[fiber_bundle F V]
[vector_bundle 𝕜 F V]
[smooth_vector_bundle F V I] :
has_smul ℕ (cont_mdiff_section I F n V)
Equations
@[simp]
theorem
cont_mdiff_section.coe_nsmul
{𝕜 : 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]
[smooth_manifold_with_corners I M]
{F : Type u_11}
[normed_add_comm_group F]
[normed_space 𝕜 F]
{n : ℕ∞}
{V : M → Type u_12}
[topological_space (bundle.total_space F V)]
[Π (x : M), add_comm_group (V x)]
[Π (x : M), module 𝕜 (V x)]
[Π (x : M), topological_space (V x)]
[fiber_bundle F V]
[vector_bundle 𝕜 F V]
[smooth_vector_bundle F V I]
(s : cont_mdiff_section I F n V)
(k : ℕ) :
@[protected, instance]
def
cont_mdiff_section.has_zsmul
{𝕜 : 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]
[smooth_manifold_with_corners I M]
{F : Type u_11}
[normed_add_comm_group F]
[normed_space 𝕜 F]
{n : ℕ∞}
{V : M → Type u_12}
[topological_space (bundle.total_space F V)]
[Π (x : M), add_comm_group (V x)]
[Π (x : M), module 𝕜 (V x)]
[Π (x : M), topological_space (V x)]
[fiber_bundle F V]
[vector_bundle 𝕜 F V]
[smooth_vector_bundle F V I] :
has_smul ℤ (cont_mdiff_section I F n V)
Equations
@[simp]
theorem
cont_mdiff_section.coe_zsmul
{𝕜 : 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]
[smooth_manifold_with_corners I M]
{F : Type u_11}
[normed_add_comm_group F]
[normed_space 𝕜 F]
{n : ℕ∞}
{V : M → Type u_12}
[topological_space (bundle.total_space F V)]
[Π (x : M), add_comm_group (V x)]
[Π (x : M), module 𝕜 (V x)]
[Π (x : M), topological_space (V x)]
[fiber_bundle F V]
[vector_bundle 𝕜 F V]
[smooth_vector_bundle F V I]
(s : cont_mdiff_section I F n V)
(z : ℤ) :
@[protected, instance]
def
cont_mdiff_section.add_comm_group
{𝕜 : 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]
[smooth_manifold_with_corners I M]
{F : Type u_11}
[normed_add_comm_group F]
[normed_space 𝕜 F]
{n : ℕ∞}
{V : M → Type u_12}
[topological_space (bundle.total_space F V)]
[Π (x : M), add_comm_group (V x)]
[Π (x : M), module 𝕜 (V x)]
[Π (x : M), topological_space (V x)]
[fiber_bundle F V]
[vector_bundle 𝕜 F V]
[smooth_vector_bundle F V I] :
add_comm_group (cont_mdiff_section I F n V)
Equations
- cont_mdiff_section.add_comm_group = function.injective.add_comm_group coe_fn cont_mdiff_section.add_comm_group._proof_1 cont_mdiff_section.add_comm_group._proof_2 cont_mdiff_section.add_comm_group._proof_3 cont_mdiff_section.add_comm_group._proof_4 cont_mdiff_section.add_comm_group._proof_5 cont_mdiff_section.add_comm_group._proof_6 cont_mdiff_section.add_comm_group._proof_7
def
cont_mdiff_section.coe_add_hom
{𝕜 : 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]
[smooth_manifold_with_corners I M]
(F : Type u_11)
[normed_add_comm_group F]
[normed_space 𝕜 F]
(n : ℕ∞)
(V : M → Type u_12)
[topological_space (bundle.total_space F V)]
[Π (x : M), add_comm_group (V x)]
[Π (x : M), module 𝕜 (V x)]
[Π (x : M), topological_space (V x)]
[fiber_bundle F V]
[vector_bundle 𝕜 F V]
[smooth_vector_bundle F V I] :
cont_mdiff_section I F n V →+ Π (x : M), V x
The additive morphism from smooth sections to dependent maps.
Equations
- cont_mdiff_section.coe_add_hom I F n V = {to_fun := coe_fn cont_mdiff_section.has_coe_to_fun, map_zero' := _, map_add' := _}
@[protected, instance]
def
cont_mdiff_section.module
{𝕜 : 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]
[smooth_manifold_with_corners I M]
{F : Type u_11}
[normed_add_comm_group F]
[normed_space 𝕜 F]
{n : ℕ∞}
{V : M → Type u_12}
[topological_space (bundle.total_space F V)]
[Π (x : M), add_comm_group (V x)]
[Π (x : M), module 𝕜 (V x)]
[Π (x : M), topological_space (V x)]
[fiber_bundle F V]
[vector_bundle 𝕜 F V]
[smooth_vector_bundle F V I] :
module 𝕜 (cont_mdiff_section I F n V)
Equations
- cont_mdiff_section.module = function.injective.module 𝕜 (cont_mdiff_section.coe_add_hom I F n V) cont_mdiff_section.module._proof_5 cont_mdiff_section.module._proof_6