mathlib documentation

core.init.data.prod

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

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

Equations
@[instance]
def prod.decidable_eq {α : Type u} {β : Type v} [h₁ : decidable_eq α] [h₂ : 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 _
@[instance]
def prod.has_lt {α : Type u} {β : Type v} [has_lt α] [has_lt β] :
has_lt × β)

Equations
@[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
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)

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

Equations