ext — Mathlib

English

Two sequences are equal if and only if all their nth elements agree, i.e., s = t iff s.get? n = t.get? n for all n.

Русский

Две последовательности равны тогда и только тогда, когда их элементы в каждой позиции совпадают: s = t тогда и только тогда, когда s.get? n = t.get? n для всех n.

LaTeX

$$$\\forall s,t:\\mathrm{Seq}\\,\\alpha,\\;\\big(\\forall n:\\mathbb{N},\\; s.\\mathrm{get?}(n)=t.\\mathrm{get?}(n)\\big)\\Rightarrow s=t,$$$

Lean4

@[ext]
protected theorem ext {s t : Seq α} (h : ∀ n : ℕ, s.get? n = t.get? n) : s = t :=
  Subtype.eq <| funext h

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