feat(data/subtype): subtype.coe_ext

leanprover-community · Sep 20, 2018 · 1758092 · 1758092
1 parent 9815239
commit 1758092
Showing 1 changed file with 3 additions and 0 deletions.
diff --git a/data/subtype.lean b/data/subtype.lean
@@ -13,6 +13,9 @@ protected lemma subtype.eq' : ∀ {a1 a2 : {x // β x}}, a1.val = a2.val → a1
 lemma subtype.ext {a1 a2 : {x // β x}} : a1 = a2 ↔ a1.val = a2.val :=
 ⟨congr_arg _, subtype.eq'⟩
 
+lemma subtype.coe_ext {a1 a2 : {x // β x}} : a1 = a2 ↔ (a1 : α) = a2 :=
+subtype.ext
+
 theorem subtype.val_injective : function.injective (@subtype.val _ β) :=
 λ a b, subtype.eq'