add — Mathlib

English

Let f and g be Cauchy sequences in β with respect to abv. Then their sum f+g is a Cauchy sequence with respect to abv.

Русский

Пусть f и g — последовательности Коши в β относительно abv. Тогда их сумма f+g является последовательностью Коши по отношению к abv.

LaTeX

$$$IsCauSeq abv f \\to IsCauSeq abv g \\to IsCauSeq abv (f+g)$$$

Lean4

theorem add (hf : IsCauSeq abv f) (hg : IsCauSeq abv g) : IsCauSeq abv (f + g) := fun _ ε0 =>
  let ⟨_, δ0, Hδ⟩ := rat_add_continuous_lemma abv ε0
  let ⟨i, H⟩ := exists_forall_ge_and (hf.cauchy₃ δ0) (hg.cauchy₃ δ0)
  ⟨i, fun _ ij =>
    let ⟨H₁, H₂⟩ := H _ le_rfl
    Hδ (H₁ _ ij) (H₂ _ ij)⟩

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