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)
350theorem differentiableAt_coordRay_i (x : Fin 4 → ℝ) (μ i : Fin 4) :
351 DifferentiableAt ℝ (fun t => (coordRay x μ t) i) 0 := by
proof body
Term-mode proof.
352 simp only [coordRay_apply]
353 apply DifferentiableAt.add
354 · apply differentiableAt_const
355 · apply DifferentiableAt.mul
356 · apply differentiableAt_id
357 · apply differentiableAt_const
358
359/-- Differentiability of a squared coordinate ray component. -/
used by (4)
From the project-wide theorem graph. These declarations reference this one in their body.
depends on (11)
Lean names referenced from this declaration's body.
-
of
in IndisputableMonolith.Astrophysics.NucleosynthesisTiers
decl_use
-
mul
in IndisputableMonolith.Foundation.ArithmeticFromLogic
decl_use
-
of
in IndisputableMonolith.Foundation.DAlembert.LedgerFactorization
decl_use
-
mul
in IndisputableMonolith.Foundation.IntegersFromLogic
decl_use
-
of
in IndisputableMonolith.Foundation.PhiForcingDerived
decl_use
-
mul
in IndisputableMonolith.Foundation.RationalsFromLogic
decl_use
-
of
in IndisputableMonolith.Foundation.SpectralEmergence
decl_use
-
of
in IndisputableMonolith.Information.PhysicsComplexityStructure
decl_use
-
mul
in IndisputableMonolith.RecogSpec.Core
decl_use
-
coordRay
in IndisputableMonolith.Relativity.Calculus.Derivatives
decl_use
-
coordRay_apply
in IndisputableMonolith.Relativity.Calculus.Derivatives
decl_use