norm_equiv — Mathlib

English

If f ≈ g, then f.norm = g.norm.

Русский

Если f эквивалентна g, то их нормы совпадают.

LaTeX

$$f.norm = g.norm \,\text{if } f \approx g$$

Lean4

theorem norm_equiv {f g : PadicSeq p} (hfg : f ≈ g) : f.norm = g.norm := by
  classical
    exact
    if hf : f ≈ 0 then by
      have hg : g ≈ 0 := Setoid.trans (Setoid.symm hfg) hf
      simp [norm, hf, hg]
    else by
      have hg : ¬g ≈ 0 := hf ∘ Setoid.trans hfg
      unfold norm; split_ifs; exact norm_eq_of_equiv hf hg hfg

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