mathlib documentation

data.pprod

Extra facts about pprod #

@[simp]
theorem pprod.mk.eta {α : Sort u_1} {β : Sort u_2} {p : pprod α β} :
p.fst, p.snd = p
@[simp]
theorem pprod.forall {α : Sort u_1} {β : Sort u_2} {p : pprod α β → Prop} :
(∀ (x : pprod α β), p x) ∀ (a : α) (b : β), p a, b⟩
@[simp]
theorem pprod.exists {α : Sort u_1} {β : Sort u_2} {p : pprod α β → Prop} :
(∃ (x : pprod α β), p x) ∃ (a : α) (b : β), p a, b⟩
theorem pprod.forall' {α : Sort u_1} {β : Sort u_2} {p : α → β → Prop} :
(∀ (x : pprod α β), p x.fst x.snd) ∀ (a : α) (b : β), p a b
theorem pprod.exists' {α : Sort u_1} {β : Sort u_2} {p : α → β → Prop} :
(∃ (x : pprod α β), p x.fst x.snd) ∃ (a : α) (b : β), p a b