norm_zero_iff — Mathlib

English

For any p, a PadicSeq f satisfies f.norm = 0 if and only if f ≈ 0 (is equivalent to zero).

Русский

Для любой p последовательность PadicSeq f имеет f.norm = 0 тогда и только тогда, когда f эквивалентна нулю.

LaTeX

$$f.norm = 0 \\Leftrightarrow f \\approx 0$$

Lean4

theorem norm_zero_iff (f : PadicSeq p) : f.norm = 0 ↔ f ≈ 0 :=
  by
  constructor
  · intro h
    by_contra hf
    unfold norm at h
    split_ifs at h
    apply hf
    intro ε hε
    exists stationaryPoint hf
    intro j hj
    have heq := stationaryPoint_spec hf le_rfl hj
    simpa [h, heq]
  · intro h
    simp [norm, h]

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