New insight mederivWithin def

urkud · Feb 7, 2025 · 370b899 · 370b899
1 parent ab37c22
commit 370b899
Show file tree

Hide file tree

Showing 2 changed files with 7 additions and 2 deletions.
diff --git a/DeRhamCohomology/Manifold/DifferentialForm.lean b/DeRhamCohomology/Manifold/DifferentialForm.lean
@@ -87,9 +87,11 @@ variable
 #check (extChartAt IM o).symm
 #check writtenInExtChartAt IM 𝓘(ℝ, (EM [⋀^Fin m]→L[ℝ] ℝ)) o α
 #check range IM
+#check 𝒜⟮ ℝ, Fin m; EM, (TangentSpace IM : M → Type _); ℝ, (Bundle.Trivial M ℝ)⟯
 
 def mederivWithin (s : Set M) (x : M) : TangentSpace IM x [⋀^Fin (m + 1)]→L[ℝ] Trivial M ℝ x :=
-    (ederivWithin (E := EM) (F := ℝ) (n := m) (writtenInExtChartAt IM 𝓘(ℝ, (EM [⋀^Fin m]→L[ℝ] ℝ)) x α)
-      ((extChartAt IM x).symm ⁻¹' s ∩ range IM)) (extChartAt IM x x)
+    (ederivWithin (E := EM) (F := ℝ) (n := m) (writtenInExtChartAt IM 𝓘(ℝ, (EM [⋀^Fin m]→L[ℝ] ℝ)) x
+      (fun (y : M) ↦ (α y : 𝒜⟮ ℝ, Fin m; EM, (TangentSpace IM : M → Type _); ℝ, (Bundle.Trivial M ℝ)⟯)))
+        ((extChartAt IM x).symm ⁻¹' s ∩ range IM)) (extChartAt IM x x)
 
 end mederiv
diff --git a/DeRhamCohomology/Manifold/VectorBundle/Alternating.lean b/DeRhamCohomology/Manifold/VectorBundle/Alternating.lean
@@ -93,4 +93,7 @@ instance SmoothVectorBundle.continuousAlternatingMap :
     SmoothVectorBundle (F₁ [⋀^ι]→L[𝕜] F₂) (Bundle.continuousAlternatingMap 𝕜 ι F₁ E₁ F₂ E₂) IB :=
   (Bundle.continuousAlternatingMap.vectorPrebundle 𝕜 ι F₁ E₁ F₂ E₂).smoothVectorBundle IB
 
+-- Notation for total space of continuous alternating bundle
+notation3 "𝒜⟮" 𝕜 "," ι ";"  F₁ "," E₁ ";"  F₂ "," E₂ "⟯" => TotalSpace (F₁ [⋀^ι]→L[𝕜] F₂) ⋀^ι⟮𝕜; F₁, E₁; F₂, E₂⟯
+
 end