No prose has been written for this declaration yet. The Lean source and graph data below render
without it.
generate prose now
formal statement (Lean)
65def SmoothField (V : ℝ → (Fin 4 → ℝ)) : Prop :=
proof body
Definition body.
66 ∀ μ, Differentiable ℝ (fun l => V l μ)
67
68/-- Initial conditions for parallel transport: a vector at parameter λ₀. -/
used by (2)
From the project-wide theorem graph. These declarations reference this one in their body.
depends on (4)
Lean names referenced from this declaration's body.
-
V
in IndisputableMonolith.Cosmology.InflatonPotentialFromJCost
decl_use
-
V
in IndisputableMonolith.Foundation.SpectralEmergence
decl_use
-
for
in IndisputableMonolith.Foundation.UniversalForcingSelfReference
decl_use
-
V
in IndisputableMonolith.RRF.Core.Glossary
decl_use