mathlib3 documentation

data.prod.pprod

Extra facts about `pprod` #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

@[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

theorem function.injective.pprod_map {α : Sort u_1} {β : Sort u_2} {γ : Sort u_3} {δ : Sort u_4} {f : α → β} {g : γ → δ} (hf : function.injective f) (hg : function.injective g) :

function.injective (λ (x : pprod α γ), ⟨f x.fst, g x.snd⟩)