def
definition
TangentVector
show as:
view math explainer →
open explainer
Generate a durable explainer page for this declaration.
open lean source
IndisputableMonolith.Relativity.Geometry.Manifold on GitHub at line 41.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
formal source
38def Point (M : Manifold) := Fin M.dim → ℝ
39
40/-- A vector at a point (tangent space). -/
41def TangentVector (M : Manifold) := Fin M.dim → ℝ
42
43/-- A covector at a point (cotangent space). -/
44def Covector (M : Manifold) := Fin M.dim → ℝ
45
46/-- Standard 4D spacetime manifold. -/
47def Spacetime : Manifold := { dim := 4 }
48
49/-- Coordinate indices for spacetime. -/
50abbrev SpacetimeIndex := Fin 4
51
52/-- Time coordinate (index 0). -/
53def timeIndex : SpacetimeIndex := 0
54
55/-- Spatial indices (1, 2, 3). -/
56def spatialIndices : List SpacetimeIndex := [1, 2, 3]
57
58/-- Check if an index is spatial. -/
59def isSpatial (μ : SpacetimeIndex) : Bool := μ ≠ 0
60
61/-- Kronecker delta for indices. -/
62def kronecker {n : ℕ} (μ ν : Fin n) : ℝ := if μ = ν then 1 else 0
63
64theorem kronecker_symm {n : ℕ} (μ ν : Fin n) :
65 kronecker μ ν = kronecker ν μ := by
66 by_cases h : μ = ν
67 · simp [kronecker, h]
68 · have h' : ν ≠ μ := by
69 intro hνμ
70 exact h hνμ.symm
71 simp [kronecker, h, h']