ext_of_localization — Mathlib

English

If two CatCenter objects r and s agree on all localized evaluations along L, i.e., r.app (L.obj X) = s.app (L.obj X) for all X, then r = s.

Русский

Если два элемента CatCenter совпадают на всех локализациях по L, то они равны.

LaTeX

$$$\forall X,\ r.app (L.obj X) = s.app (L.obj X) \Rightarrow r = s$$$

Lean4

theorem ext_of_localization (r s : CatCenter D) (h : ∀ (X : C), r.app (L.obj X) = s.app (L.obj X)) : r = s :=
  Localization.natTrans_ext L W h

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