feat: add Nonempty instances for products

leanprover · Sep 17, 2024 · 2561b75 · 2561b75
1 parent c25d206
commit 2561b75
Showing 1 changed file with 15 additions and 0 deletions.
diff --git a/src/Init/Core.lean b/src/Init/Core.lean
@@ -1191,6 +1191,21 @@ end
 
 /-! # Product -/
 
+instance [h1 : Nonempty α] [h2 : Nonempty β] : Nonempty (α × β) :=
+  Nonempty.elim h1 fun x =>
+    Nonempty.elim h2 fun y =>
+      ⟨(x, y)⟩
+
+instance [h1 : Nonempty α] [h2 : Nonempty β] : Nonempty (MProd α β) :=
+  Nonempty.elim h1 fun x =>
+    Nonempty.elim h2 fun y =>
+      ⟨⟨x, y⟩⟩
+
+instance [h1 : Nonempty α] [h2 : Nonempty β] : Nonempty (PProd α β) :=
+  Nonempty.elim h1 fun x =>
+    Nonempty.elim h2 fun y =>
+      ⟨⟨x, y⟩⟩
+
 instance [Inhabited α] [Inhabited β] : Inhabited (α × β) where
   default := (default, default)