• to_fun : ℝ → E → E
• t_min : ℝ
• t_max : ℝ
• t₀ : ↥(set.Icc self.t_min self.t_max)
• x₀ : E
• C : nnreal
• R : nnreal
• L : nnreal
• lipschitz' : ∀ (t : ℝ), t ∈ set.Icc self.t_min self.t_max → lipschitz_on_with self.L (self.to_fun t) (metric.closed_ball self.x₀ ↑(self.R))
• cont : ∀ (x : E), x ∈ metric.closed_ball self.x₀ ↑(self.R) → continuous_on (λ (t : ℝ), self.to_fun t x) (set.Icc self.t_min self.t_max)
• norm_le' : ∀ (t : ℝ), t ∈ set.Icc self.t_min self.t_max → ∀ (x : E), x ∈ metric.closed_ball self.x₀ ↑(self.R) → ∥self.to_fun t x∥ ≤ ↑(self.C)
• C_mul_le_R : ↑(self.C) * linear_order.max (self.t_max - ↑(self.t₀)) (↑(self.t₀) - self.t_min) ≤ ↑(self.R)

This structure holds arguments of the Picard-Lipschitz (Cauchy-Lipschitz) theorem. Unless you want to use one of the auxiliary lemmas, use exists_forall_deriv_within_Icc_eq_of_lipschitz_of_continuous instead of using this structure.

• to_fun : ↥(set.Icc v.t_min v.t_max) → E
• map_t₀' : self.to_fun v.t₀ = v.x₀
• lipschitz' : lipschitz_with v.C self.to_fun

The space of curves $γ \colon [t_{\min}, t_{\max}] \to E$ such that $γ(t₀) = x₀$ and $γ$ is Lipschitz continuous with constant $C$. The map sending $γ$ to $\mathbf Pγ(t)=x₀ + ∫_{t₀}^{t} v(τ, γ(τ))\,dτ$ is a contracting map on this space, and its fixed point is a solution of the ODE $\dot x=v(t, x)$.