gronwallBound_ε0_δ0

Mathlib.Analysis.ODE.Gronwall

URI: https://scilib.ai/kg/mathlib#gronwallBound_ε0_δ0

English

If both δ and ε are zero, gronwallBound becomes identically zero: gronwallBound(0,K,0,x) = 0 for all x.

Русский

Если δ = 0 и ε = 0, граница Гронвалла тождественно равна нулю: G(0,K,0,x)=0.

LaTeX

$$$\operatorname{gronwallBound}(0,K,0,x)=0$$$

Lean4

theorem gronwallBound_ε0_δ0 (K x : ℝ) : gronwallBound 0 K 0 x = 0 := by simp only [gronwallBound_ε0, zero_mul]

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru