mathlib documentation

data.prod

Extra facts about `prod`

This file defines prod.swap : α × β → β × α and proves various simple lemmas about prod.

@[simp]

theorem prod.forall {α : Type u_1} {β : Type u_2} {p : α × β → Prop} :

(∀ (x : α × β), p x) ↔ ∀ (a : α) (b : β), p (a, b)

@[simp]

theorem prod.exists {α : Type u_1} {β : Type u_2} {p : α × β → Prop} :

(∃ (x : α × β), p x) ↔ ∃ (a : α) (b : β), p (a, b)

@[simp]

theorem prod_map {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} (f : α → γ) (g : β → δ) (p : α × β) :

prod.map f g p = (f p.fst, g p.snd)

@[simp]

theorem prod.map_mk {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} (f : α → γ) (g : β → δ) (a : α) (b : β) :

prod.map f g (a, b) = (f a, g b)

theorem prod.map_fst {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} (f : α → γ) (g : β → δ) (p : α × β) :

(prod.map f g p).fst = f p.fst

theorem prod.map_snd {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} (f : α → γ) (g : β → δ) (p : α × β) :

(prod.map f g p).snd = g p.snd

theorem prod.map_fst' {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} (f : α → γ) (g : β → δ) :

prod.fst ∘ prod.map f g = f ∘ prod.fst

theorem prod.map_snd' {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} (f : α → γ) (g : β → δ) :

prod.snd ∘ prod.map f g = g ∘ prod.snd

@[simp]

theorem prod.mk.inj_iff {α : Type u_1} {β : Type u_2} {a₁ a₂ : α} {b₁ b₂ : β} :

(a₁, b₁) = (a₂, b₂) ↔ a₁ = a₂ ∧ b₁ = b₂

theorem prod.mk.inj_left {α : Type u_1} {β : Type u_2} (a : α) :

function.injective (prod.mk a)

theorem prod.mk.inj_right {α : Type u_1} {β : Type u_2} (b : β) :

function.injective (λ (a : α), (a, b))

theorem prod.ext_iff {α : Type u_1} {β : Type u_2} {p q : α × β} :

p = q ↔ p.fst = q.fst ∧ p.snd = q.snd

@[ext]

theorem prod.ext {α : Type u_1} {β : Type u_2} {p q : α × β} (h₁ : p.fst = q.fst) (h₂ : p.snd = q.snd) :

p = q

theorem prod.map_def {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} {f : α → γ} {g : β → δ} :

prod.map f g = λ (p : α × β), (f p.fst, g p.snd)

theorem prod.id_prod {α : Type u_1} :

(λ (p : α × α), (p.fst, p.snd)) = id

theorem prod.fst_surjective {α : Type u_1} {β : Type u_2} [h : nonempty β] :

function.surjective prod.fst

theorem prod.snd_surjective {α : Type u_1} {β : Type u_2} [h : nonempty α] :

function.surjective prod.snd

theorem prod.fst_injective {α : Type u_1} {β : Type u_2} [subsingleton β] :

function.injective prod.fst

theorem prod.snd_injective {α : Type u_1} {β : Type u_2} [subsingleton α] :

function.injective prod.snd

def prod.swap {α : Type u_1} {β : Type u_2} (a : α × β) :

β × α

Swap the factors of a product. swap (a, b) = (b, a)

Equations

prod.swap = λ (p : α × β), (p.snd, p.fst)

@[simp]

theorem prod.swap_swap {α : Type u_1} {β : Type u_2} (x : α × β) :

x.swap.swap = x

@[simp]

theorem prod.fst_swap {α : Type u_1} {β : Type u_2} {p : α × β} :

p.swap.fst = p.snd

@[simp]

theorem prod.snd_swap {α : Type u_1} {β : Type u_2} {p : α × β} :

p.swap.snd = p.fst

@[simp]

theorem prod.swap_prod_mk {α : Type u_1} {β : Type u_2} {a : α} {b : β} :

(a, b).swap = (b, a)

@[simp]

theorem prod.swap_swap_eq {α : Type u_1} {β : Type u_2} :

prod.swap ∘ prod.swap = id

@[simp]

theorem prod.swap_left_inverse {α : Type u_1} {β : Type u_2} :

function.left_inverse prod.swap prod.swap

@[simp]

theorem prod.swap_right_inverse {α : Type u_1} {β : Type u_2} :

function.right_inverse prod.swap prod.swap

theorem prod.eq_iff_fst_eq_snd_eq {α : Type u_1} {β : Type u_2} {p q : α × β} :

p = q ↔ p.fst = q.fst ∧ p.snd = q.snd

theorem prod.fst_eq_iff {α : Type u_1} {β : Type u_2} {p : α × β} {x : α} :

p.fst = x ↔ p = (x, p.snd)

theorem prod.snd_eq_iff {α : Type u_1} {β : Type u_2} {p : α × β} {x : β} :

p.snd = x ↔ p = (p.fst, x)

theorem prod.lex_def {α : Type u_1} {β : Type u_2} (r : α → α → Prop) (s : β → β → Prop) {p q : α × β} :

prod.lex r s p q ↔ r p.fst q.fst ∨ p.fst = q.fst ∧ s p.snd q.snd

@[instance]

def prod.lex.decidable {α : Type u_1} {β : Type u_2} [decidable_eq α] (r : α → α → Prop) (s : β → β → Prop) [decidable_rel r] [decidable_rel s] :

decidable_rel (prod.lex r s)

Equations

prod.lex.decidable r s = λ (p q : α × β), decidable_of_decidable_of_iff or.decidable _

theorem function.injective.prod_map {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} {f : α → γ} {g : β → δ} (hf : function.injective f) (hg : function.injective g) :

function.injective (prod.map f g)

theorem function.surjective.prod_map {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} {f : α → γ} {g : β → δ} (hf : function.surjective f) (hg : function.surjective g) :

function.surjective (prod.map f g)