instance instLawfulBEqProd {α : Type u_1} {β : Type u_2} [BEq α] [BEq β] [LawfulBEq α] [LawfulBEq β] : LawfulBEq (α × β)

Equations

• ⋯ = ⋯

@[simp]

theorem Prod.forall {α : Type u_1} {β : Type u_2} {p : α × β → Prop} : (∀ (x : α × β), p x) ↔ ∀ (a : α) (b : β), p (a, b)

@[simp]

theorem Prod.exists {α : Type u_1} {β : Type u_2} {p : α × β → Prop} : (∃ (x : α × β), p x) ↔ ∃ (a : α), ∃ (b : β), p (a, b)