English
Let f and g be Cauchy sequences in β with respect to abv. Then their product 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 mul (hf : IsCauSeq abv f) (hg : IsCauSeq abv g) : IsCauSeq abv (f * g) := fun _ ε0 =>
let ⟨_, _, hF⟩ := hf.bounded' 0
let ⟨_, _, hG⟩ := hg.bounded' 0
let ⟨_, δ0, Hδ⟩ := rat_mul_continuous_lemma abv ε0
let ⟨i, H⟩ := exists_forall_ge_and (hf.cauchy₃ δ0) (hg.cauchy₃ δ0)
⟨i, fun j ij =>
let ⟨H₁, H₂⟩ := H _ le_rfl
Hδ (hF j) (hG i) (H₁ _ ij) (H₂ _ ij)⟩
