isMIntegralCurve_const — Mathlib

English

For Ne a 0, IsMIntegralCurve γ v t0 is equivalent to IsMIntegralCurve (γ ∘ (· * a)) (a • v) (t0 / a). This emphasizes the equivalence under nonzero time-scaling.

Русский

При Ne a 0: IsMIntegralCurve γ v t0 эквивалентно IsMIntegralCurve (γ ∘ (· * a)) (a • v) (t0 / a).

LaTeX

$$$IsMIntegralCurve(\\gamma, v, t_0) \\iff IsMIntegralCurve(\\gamma \\circ (\\cdot * a), a \\cdot v, t_0 / a)$$$

Lean4

/-- If the vector field `v` vanishes at `x₀`, then the constant curve at `x₀`
is a global integral curve of `v`. -/
theorem isMIntegralCurve_const {x : M} (h : v x = 0) : IsMIntegralCurve (fun _ ↦ x) v :=
  by
  intro t
  rw [h, ← ContinuousLinearMap.zero_apply (R₁ := ℝ) (R₂ := ℝ) (1 : ℝ), ContinuousLinearMap.smulRight_one_one]
  exact hasMFDerivAt_const ..

Похожие утверждения