cau_seq_zero_ne_one — Mathlib

English

The zero Cauchy sequence is not equivalent to the constant one sequence in CauSeq.Completion.

Русский

Нулевая последовательность Коши не эквивалентна константной единице в CauSeq.Completion.

LaTeX

$$¬(0 : CauSeq _ abv) ≈ 1$$

Lean4

theorem cau_seq_zero_ne_one : ¬(0 : CauSeq _ abv) ≈ 1 := fun h =>
  have : LimZero (1 - 0 : CauSeq _ abv) := Setoid.symm h
  have : LimZero (1 : CauSeq _ abv) := by simpa
  by apply one_ne_zero <| const_limZero.1 this

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