limit_ext' — Mathlib

English

Extensionality for limits: two limits are equal iff their projections agree on every index.

Русский

Экстенсиональность для предела: два предела равны тогда и только тогда, когда их проекции совпадают на каждом индексе.

LaTeX

$$$\forall J\,[Category]\ F\ :,\; (x,y: \lim F) \; (\forall j, \pi_F j x = \pi_F j y) \Rightarrow x=y.$$$

Lean4

@[ext]
theorem limit_ext' (F : J ⥤ Type v) (x y : limit F) (w : ∀ j, limit.π F j x = limit.π F j y) : x = y :=
  limit_ext F x y w

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