442theorem spatialRadius_coordRay_ne_zero_eventually {x : Fin 4 → ℝ} (hx : spatialRadius x ≠ 0) (μ : Fin 4) : 443 ∀ᶠ t in 𝓝 0, spatialRadius (coordRay x μ t) ≠ 0 := by
proof body
Tactic-mode proof.
444 have h_cont : Continuous (fun t => spatialRadius (coordRay x μ t)) := by 445 unfold spatialRadius spatialNormSq coordRay basisVec 446 fun_prop 447 apply h_cont.continuousAt.eventually_ne 448 simp [coordRay_zero, hx] 449 450/-- Directional derivative of `spatialRadius` in coordinates. 451 452 For temporal direction (μ = 0), the spatial radius is invariant along the 453 coordinate ray, so the derivative is 0. For a spatial direction (μ ≠ 0), 454 we compose the chain rule for `Real.sqrt` (Mathlib `HasDerivAt.sqrt`) 455 with the derivative `∂_μ ‖x‖² = 2 x_μ` (lifted from 456 `partialDeriv_v2_spatialNormSq`), giving `(2 x_μ) / (2 √‖x‖²) = x_μ / r`. 457 458 Closes one of the seven §XXIII.B′ Mathlib calculus axioms. -/
used by (4)
From the project-wide theorem graph. These declarations reference this one in their body.