term_congr — Mathlib

English

If f and g agree for all n ≠ 0, then term f s n = term g s n for every s and n.

Русский

Если f и g совпадают для всех n ≠ 0, то term f s n = term g s n для любых s и n.

LaTeX

$$$\\bigl( \\forall {n}, n \\neq 0 \\Rightarrow f(n) = g(n) \\bigr) \\Rightarrow \\forall s n, \\operatorname{term}(f,s,n) = \\operatorname{term}(g,s,n)$$$

Lean4

theorem term_congr {f g : ℕ → ℂ} (h : ∀ {n}, n ≠ 0 → f n = g n) (s : ℂ) (n : ℕ) : term f s n = term g s n := by
  rcases eq_or_ne n 0 with hn | hn <;> simp [hn, h]

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