Documentation

Mathlib.Data.Prod.PProd

Extra facts about PProd #

def PProd.mk.injArrow {α : Type u_5} {β : Type u_6} {x₁ : α} {y₁ : β} {x₂ : α} {y₂ : β} :
(x₁, y₁) = (x₂, y₂)P : Sort u_7⦄ → (x₁ = x₂y₁ = y₂P)P
Equations
@[simp]
theorem PProd.mk.eta {α : Sort u_1} {β : Sort u_2} {p : α ×' β} :
p.fst, p.snd = p
@[simp]
theorem PProd.forall {α : Sort u_1} {β : Sort u_2} {p : α ×' βProp} :
(∀ (x : α ×' β), p x) ∀ (a : α) (b : β), p a, b
@[simp]
theorem PProd.exists {α : Sort u_1} {β : Sort u_2} {p : α ×' βProp} :
(∃ (x : α ×' β), p x) ∃ (a : α), ∃ (b : β), p a, b
theorem PProd.forall' {α : Sort u_1} {β : Sort u_2} {p : αβProp} :
(∀ (x : α ×' β), p x.fst x.snd) ∀ (a : α) (b : β), p a b
theorem PProd.exists' {α : Sort u_1} {β : Sort u_2} {p : αβProp} :
(∃ (x : α ×' β), 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 fun (x : α ×' γ) => f x.fst, g x.snd