ext — Mathlib

English

RelSeries is determined by its length and its indexed values; two series are equal if these coincide.

Русский

RelSeries определяется длиной и значениями по индексам; две последовательности равны, если эти данные совпадают.

LaTeX

$$$ x.length = y.length \\land x.toFun = y.toFun \\circ \\mathrm{Fin.cast} (\\text{proof}) \\Rightarrow x = y. $$$

Lean4

@[ext (iff := false)]
theorem ext {x y : RelSeries r} (length_eq : x.length = y.length)
    (toFun_eq : x.toFun = y.toFun ∘ Fin.cast (by rw [length_eq])) : x = y :=
  by
  rcases x with ⟨nx, fx⟩
  dsimp only at length_eq
  subst length_eq
  simp_all

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