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