reverse — Mathlib

English

The time-reversal of a flow ϕ when the group is commutative is defined by (ϕ.reverse) t x = ϕ(-t) x.

Русский

Обратное во времени преобразование потока ϕ определяется как (ϕ.reverse) t x = ϕ(-t) x.

LaTeX

$$$\\text{reverse}(\\\\varphi) (t, x) = \\\\varphi(-t, x).$$$

Lean4

/-- The time-reversal of a flow `ϕ` by a (commutative, additive) group
is defined `ϕ.reverse t x = ϕ (-t) x`. -/
def reverse : Flow τ α where
  toFun t := ϕ (-t)
  cont' := ϕ.continuous continuous_fst.neg continuous_snd
  map_add' _ _ _ := by rw [neg_add, map_add]
  map_zero' _ := by rw [neg_zero, map_zero_apply]

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