eq_on_nat_iff_eq_on_int — Mathlib

English

For any f,g : AbsoluteValue R S, f(n) = g(n) for all n ∈ ℕ if and only if f(z) = g(z) for all z ∈ ℤ.

Русский

Для любых f,g : AbsoluteValue R S, равны на натуральных аргументах тогда и только тогда, когда равны на целых аргументах.

LaTeX

$$$(\\forall n \\in \\mathbb{N}, f(n) = g(n)) \\iff (\\forall z \\in \\mathbb{Z}, f(z) = g(z))$$$

Lean4

/-- Values of an absolute value coincide on the image of `ℕ` in `R`
if and only if they coincide on the image of `ℤ` in `R`. -/
theorem eq_on_nat_iff_eq_on_int {f g : AbsoluteValue R S} : (∀ n : ℕ, f n = g n) ↔ ∀ n : ℤ, f n = g n :=
  by
  refine ⟨fun h z ↦ ?_, fun a n ↦ mod_cast a n⟩
  obtain ⟨n, rfl | rfl⟩ := Int.eq_nat_or_neg z <;> simp [h n]

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