feat(data/pi): add pi.single_inj (#10644)

leanprover-community · Dec 7, 2021 · 9a2c299 · 9a2c299
1 parent 03dd404
commit 9a2c299
Showing 1 changed file with 3 additions and 0 deletions.
diff --git a/src/data/pi.lean b/src/data/pi.lean
@@ -137,6 +137,9 @@ variables (f)
 lemma single_injective (i : I) : function.injective (single i : f i → Π i, f i) :=
 function.update_injective _ i
 
+@[simp] lemma single_inj (i : I) {x y : f i} : pi.single i x = pi.single i y ↔ x = y :=
+(pi.single_injective _ _).eq_iff
+
 end
 end pi