abbrev definition def or abbrev

`RealAction`

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

formal statement (Lean)

  40abbrev RealAction := ℝ → ℝ

Definition body.

  41
  42/-- Time translation by `dt` on real-valued trajectories. -/

From the project-wide theorem graph. These declarations reference this one in their body.

isSpaceTranslationInvariant in IndisputableMonolith.Action.Noether decl_use
isTimeTranslationInvariant in IndisputableMonolith.Action.Noether decl_use
spaceShift in IndisputableMonolith.Action.Noether decl_use
spaceTranslationFlow in IndisputableMonolith.Action.Noether decl_use
space_translation_invariance_implies_momentum_conservation in IndisputableMonolith.Action.Noether decl_use
timeShift in IndisputableMonolith.Action.Noether decl_use
timeTranslationFlow in IndisputableMonolith.Action.Noether decl_use
time_translation_invariance_implies_energy_conservation in IndisputableMonolith.Action.Noether decl_use

Lean names referenced from this declaration's body.