def
definition
Point
show as:
view math explainer →
open explainer
Read the cached plain-language explainer.
open lean source
IndisputableMonolith.Relativity.Geometry.Manifold on GitHub at line 38.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
used by
formal source
35 deriving Repr
36
37/-- A point on the manifold (coordinates). -/
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