mathlib documentation

core.init.data.prod

source
@[simp]
theorem prod.mk.eta {α : Type u} {β : Type v} {p : α × β} :
(p.fst, p.snd) = p

source
@[instance]
def prod.inhabited {α : Type u} {β : Type v} [inhabited α] [inhabited β] :
inhabited (α × β)

Equations
source
@[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
@[instance]
def prod.has_lt {α : Type u} {β : Type v} [has_lt α] [has_lt β] :
has_lt (α × β)

Equations
source
@[instance]
def prod_has_decidable_lt {α : Type u} {β : Type v} [has_lt α] [has_lt β] [decidable_eq α] [decidable_eq β] [decidable_rel has_lt.lt] [decidable_rel has_lt.lt] (s t : α × β) :
decidable (s < t)

Equations
source
theorem prod.lt_def {α : Type u} {β : Type v} [has_lt α] [has_lt β] (s t : α × β) :
s < t = (s.fst < t.fst ∨ s.fst = t.fst ∧ s.snd < t.snd)

source
def prod.map {α₁ : Type u₁} {α₂ : Type u₂} {β₁ : Type v₁} {β₂ : Type v₂} (f : α₁ → α₂) (g : β₁ → β₂) (x : α₁ × β₁) :
α₂ × β₂

Equations