mathlib documentation

core / init.data.prod

source
@[simp]
theorem prod.mk.eta {α : Type u} {β : Type v} {p : α × β} :
(p.fst, p.snd) = p
source
@[protected, instance]
def prod.inhabited {α : Type u} {β : Type v} [inhabited α] [inhabited β] :
inhabited (α × β)
Equations
source
@[protected, instance]
def prod.decidable_eq {α : Type u} {β : Type v} [h₁ : decidable_eq α] [h₂ : decidable_eq β] :
decidable_eq (α × β)
Equations
  • prod.decidable_eq (a, b) (a', b') = prod.decidable_eq._match_1 a b a' b' (h₁ a a')
  • prod.decidable_eq._match_1 a b a' b' (is_true e₁) = prod.decidable_eq._match_2 a b a' b' e₁ (h₂ b b')
  • prod.decidable_eq._match_1 a b a' b' (is_false n₁) = is_false _
  • prod.decidable_eq._match_2 a b a' b' e₁ (is_true e₂) = is_true _
  • prod.decidable_eq._match_2 a b a' b' e₁ (is_false n₂) = is_false _
source
def prod.map {α₁ : Type u₁} {α₂ : Type u₂} {β₁ : Type v₁} {β₂ : Type v₂} (f : α₁ → α₂) (g : β₁ → β₂) (x : α₁ × β₁) :
α₂ × β₂
Equations