isCauSeq_norm — Mathlib

English

Reaffirmation: IsCauSeq norm f implies IsCauSeq abs (norm ∘ f).

Русский

Повторное утверждение: IsCauSeq norm f ⇒ IsCauSeq abs (norm ∘ f).

LaTeX

$$$$ \\text{IsCauSeq norm } f \\Rightarrow \\text{IsCauSeq abs } (\\|f\\|). $$$$

Lean4

theorem isCauSeq_norm {f : ℕ → K} (hf : IsCauSeq norm f) : IsCauSeq abs (norm ∘ f) := fun ε ε0 =>
  let ⟨i, hi⟩ := hf ε ε0
  ⟨i, fun j hj => lt_of_le_of_lt (abs_norm_sub_norm_le _ _) (hi j hj)⟩

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