comp_lim_obj_ext — Mathlib

English

Two elements of a lifted limit (G ⋙ lim).obj j are equal iff their projections onto each component agree.

Русский

Два элемента лимита, полученного по каскадному композиционному пределу, равны тогда и только тогда, когда их проекции совпадают на каждом компоненте.

LaTeX

$$$\forall j, x,y \in (G \!\downarrow\! lim).\!\mathrm{obj}\, j,\; (\forall k, \lim\!_{(G.obj j)} k (x) = \lim\!_{(G.obj j)} k (y)) \Rightarrow x = y$$$

Lean4

/-- `(G ⋙ lim).obj j` = `limit (G.obj j)` definitionally, so this
is just a variant of `limit_ext'`. -/
@[ext]
theorem comp_lim_obj_ext {j : J} {G : J ⥤ K ⥤ Type v} (x y : (G ⋙ lim).obj j)
    (w : ∀ (k : K), limit.π (G.obj j) k x = limit.π (G.obj j) k y) : x = y :=
  limit_ext _ x y w

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