continuousOn_uncurry — Mathlib

English

In the time-independent setting (a fixed zero time interval), there exists a fixed point α of next, i.e., next has a fixed curve solution.

Русский

В стационарном случае существует неподвижная точка для next, то есть существует неподвижная кривая решения.

LaTeX

$$$\\exists α:\\ IsFixedPt\\ (\\text{next } hf hx)\\ α.$$$

Lean4

theorem continuousOn_uncurry (hf : IsPicardLindelof f t₀ x₀ a r L K) :
    ContinuousOn (uncurry f) ((Icc tmin tmax) ×ˢ (closedBall x₀ a)) :=
  continuousOn_prod_of_continuousOn_lipschitzOnWith' _ K hf.lipschitzOnWith hf.continuousOn

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