Coverage of nonnegative time by uniform continuation intervals

A fixed positive continuation step covers every finite nonnegative time after finitely many restarts.

theorem CKN.Leray.regularisedUniformStepGrid_cover (δ t : ℝ) (hδ : 0 < δ) (ht : 0 ≤ t) : ∃ (n : ℕ), ↑n * δ ≤ t ∧ t ≤ ↑(n + 1) * δ

Every nonnegative time lies in a closed interval between consecutive multiples of a fixed positive step.