ofEq — Mathlib

English

Given a Cauchy sequence f, create a CauSeq from a sequence g that has the same values as f.

Русский

Пусть имеется последовательность Коши f; построим CauSeq из последовательности g, имеющей те же значения, что и f.

LaTeX

$$$\\operatorname{ofEq}(f,g,e) \\in CauSeq(β,abv)$, где $e(i): f(i)=g(i)$$$

Lean4

/-- Given a Cauchy sequence `f`, create a Cauchy sequence from a sequence `g` with
the same values as `f`. -/
def ofEq (f : CauSeq β abv) (g : ℕ → β) (e : ∀ i, f i = g i) : CauSeq β abv :=
  ⟨g, fun ε => by rw [show g = f from (funext e).symm]; exact f.cauchy⟩

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