unfold forwardEuler
R : Type u_1
inst✝³ : RCLike R
X : Type u_2
inst✝² : Vec R X
Y : Type ?u.676
inst✝¹ : Vec R Y
Z : Type ?u.688
inst✝ : Vec R Z
f : R → X → X
⊢ ∀ (t : R) (x : X), (Filter.limit (nhds 0) fun Δt' => ∂ (Δt:=Δt'), forwardEuler f t Δt x) = f t x
R : Type u_1
inst✝³ : RCLike R
X : Type u_2
inst✝² : Vec R X
Y : Type ?u.676
inst✝¹ : Vec R Y
Z : Type ?u.688
inst✝ : Vec R Z
f : R → X → X
⊢ ∀ (t : R) (x : X), (Filter.limit (nhds 0) fun Δt' => ∂ (Δt:=Δt'), (x + Δt • f t x)) = f t x