equiv_zero_of_val_eq_of_equiv_zero

English

If two PadicSeq f and g have equal termwise p-adic norms and f ≈ 0, then g ≈ 0.

Русский

Если две PadicSeq f и g имеют одинаковые по каждому члену нормы p и f ≈ 0, тогда g ≈ 0.

LaTeX

$$∀ f,g, (∀ k, |f(k)|_p = |g(k)|_p) → (f ≈ 0) → (g ≈ 0)$$

Lean4

theorem equiv_zero_of_val_eq_of_equiv_zero {f g : PadicSeq p} (h : ∀ k, padicNorm p (f k) = padicNorm p (g k))
    (hf : f ≈ 0) : g ≈ 0 := fun ε hε ↦
  let ⟨i, hi⟩ := hf _ hε
  ⟨i, fun j hj ↦ by simpa [h] using hi _ hj⟩

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