limit_ext — Mathlib

English

If two elements of the limit have identical coordinates in all indices, then they are equal (extensionality for the limit).

Русский

Если два элемента предела имеют одинаковые координаты во всех индексах, то они равны (ext-подобие для предела).

LaTeX

$$$\forall x,y \in \mathrm{limit}(F),\ (\forall j, x_j = y_j) \Rightarrow x = y$$$

Lean4

@[ext]
theorem limit_ext (x y : limit F) (hxy : ∀ j, x.val j = y.val j) : x = y :=
  Subtype.ext (funext hxy)

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