`BookProof.ChapterE4.wave_eq_zero_of_lt` (θ : ℕ → ℝ) (s d i : ℕ) (h : i < s) : wave θ s d i = 0
ProvedBookProof.ChapterE4.wave_eq_zero_of_lttheoremstimepiece
Prove the following Lean 4 theorem from ChapterE4.
BookProof.ChapterE4.wave_eq_zero_of_lt (θ : ℕ → ℝ) (s d i : ℕ) (h : i < s) : wave θ s d i = 0
Formalization note: Lean 4 identifier BookProof.ChapterE4.wave_eq_zero_of_lt.
Preamble
-- Generated from ChapterE4.lean — theorem BookProof.ChapterE4.wave_eq_zero_of_lt import Mathlib import Definitions.Def_ChapterE4 open BookProof.ChapterE4 open scoped BigOperators
Formal statement
theorem BookProof.ChapterE4.wave_eq_zero_of_lt (θ : ℕ → ℝ) (s d i : ℕ) (h : i < s) : wave θ s d i = 0 := by sorry