limit_ext — Mathlib

English

Two elements of the limit are equal if their components agree at every index.

Русский

Два элемента предела равны, если их компоненты совпадают на каждом индексе.

LaTeX

$$$\forall x,y: \lim F,\ (\forall j, \pi_F j x = \pi_F j y) \Rightarrow x=y.$$$

Lean4

@[ext]
theorem limit_ext (x y : limit F) (w : ∀ j, limit.π F j x = limit.π F j y) : x = y :=
  by
  apply (limitEquivSections F).injective
  ext j
  simp [w j]

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