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

• PProd.mk.injArrow h₁ h₂ = Prod.noConfusion h₁ h₂

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