mul_equiv_zero' — Mathlib

English

Let f and g be Cauchy sequences valued via abv. If f is equivalent to 0, then f multiplied by g is equivalent to 0.

Русский

Пусть f и g — последовательности Кауса, образы по abv. Если f эквивалентна нулю, то произведение f на g эквивалентно нулю.

LaTeX

$$$ \forall g\, (f \approx 0 \Rightarrow f \cdot g \approx 0) $$$

Lean4

theorem mul_equiv_zero' (g : CauSeq _ abv) {f : CauSeq _ abv} (hf : f ≈ 0) : f * g ≈ 0 :=
  have : LimZero (f - 0) := hf
  have : LimZero (f * g) := mul_limZero_left _ <| by simpa
  show LimZero (f * g - 0) by simpa

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