feat(category_theory/limits/types): ext iff lemma (#4883)

A little lemma which sometimes makes it easier to work with limits in type.
leanprover-community · Nov 3, 2020 · b37d4a3 · b37d4a3
1 parent 6bed7d4
commit b37d4a3
Showing 1 changed file with 4 additions and 0 deletions.
diff --git a/src/category_theory/limits/types.lean b/src/category_theory/limits/types.lean
@@ -104,6 +104,10 @@ begin
   simp [w j],
 end
 
+lemma limit_ext_iff (F : J ⥤ Type u) (x y : limit F) :
+  x = y ↔ (∀ j, limit.π F j x = limit.π F j y) :=
+⟨λ 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?