limit_ext_iff' — Mathlib

English

The limit is determined by its projections: equality of two limits is equivalent to equality of all their projections.

Русский

Предел определяется своими проекциями: равенство двух пределов эквивалентно равенству всех их проекций.

LaTeX

$$$x = y \;\iff\; \forall j, \pi_F j x = \pi_F j y.$$$

Lean4

theorem limit_ext_iff' (F : J ⥤ Type v) (x y : limit F) : x = y ↔ ∀ j, limit.π F j x = limit.π F j y :=
  ⟨fun t _ => t ▸ rfl, limit_ext' _ _ _⟩
    -- TODO: are there other limits lemmas that should have `_apply` versions?
    -- Can we generate these like with `@[reassoc]`?
    -- PROJECT: prove these for any concrete category where the forgetful functor preserves limits?

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