gronwallBound_continuous_ε — Mathlib

English

For fixed δ and K, the map ε ↦ gronwallBound(δ,K,ε,x) is a continuous function of ε for each x.

Русский

При фиксированных δ и K отображение ε ↦ gronwallBound(δ,K,ε,x) непрерывно по ε для каждого x.

LaTeX

$$$\varepsilon \mapsto \operatorname{gronwallBound}(\delta,K,\varepsilon,x)$ is continuous for every x.$$

Lean4

theorem gronwallBound_continuous_ε (δ K x : ℝ) : Continuous fun ε => gronwallBound δ K ε x :=
  by
  by_cases hK : K = 0
  · simp only [gronwallBound_K0, hK]
    exact continuous_const.add (continuous_id.mul continuous_const)
  · simp only [gronwallBound_of_K_ne_0 hK]
    exact continuous_const.add ((continuous_id.mul continuous_const).mul continuous_const)

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