# Documentation

Mathlib.Data.Prod.Basic

# Extra facts about prod#

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

@[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.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)
theorem Prod.forall' {α : Type u_1} {β : Type u_2} {p : αβProp} :
((x : α × β) → p x.fst x.snd) (a : α) → (b : β) → p a b
theorem Prod.exists' {α : Type u_1} {β : Type u_2} {p : αβProp} :
(x, p x.fst x.snd) a b, p a b
@[simp]
theorem Prod.snd_comp_mk {α : Type u_2} {β : Type u_1} (x : α) :
Prod.snd = id
@[simp]
theorem Prod.fst_comp_mk {α : Type u_1} {β : Type u_2} (x : α) :
Prod.fst =
@[simp]
theorem Prod.map_mk {α : Type u_3} {β : Type u_4} {γ : Type u_1} {δ : Type u_2} (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_4} {δ : Type u_3} (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_4} {δ : Type u_3} (f : αγ) (g : βδ) :
Prod.snd Prod.map f g = g Prod.snd
theorem Prod.map_comp_map {α : Type u_3} {β : Type u_6} {γ : Type u_4} {δ : Type u_5} {ε : Type u_1} {ζ : Type u_2} (f : αβ) (f' : γδ) (g : βε) (g' : δζ) :
Prod.map g g' Prod.map f f' = Prod.map (g f) (g' f')

Composing a Prod.map with another Prod.map is equal to a single Prod.map of composed functions.

theorem Prod.map_map {α : Type u_3} {β : Type u_5} {γ : Type u_4} {δ : Type u_6} {ε : Type u_1} {ζ : Type u_2} (f : αβ) (f' : γδ) (g : βε) (g' : δζ) (x : α × γ) :
Prod.map g g' (Prod.map f f' x) = Prod.map (g f) (g' f') x

Composing a Prod.map with another Prod.map is equal to a single Prod.map of composed functions, fully applied.

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 : α) :
theorem Prod.mk.inj_right {α : Type u_1} {β : Type u_2} (b : β) :
Function.Injective fun a => (a, b)
theorem Prod.mk_inj_left :
∀ {α : Type u_1} {a : α} {β : Type u_2} {b₁ b₂ : β}, (a, b₁) = (a, b₂) b₁ = b₂
theorem Prod.mk_inj_right :
∀ {α : Type u_1} {a₁ : α} {β : Type u_2} {b : β} {a₂ : α}, (a₁, b) = (a₂, b) a₁ = a₂
theorem Prod.ext_iff {α : Type u_1} {β : Type u_2} {p : α × β} {q : α × β} :
p = q p.fst = q.fst p.snd = q.snd
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 = fun p => (f p.fst, g p.snd)
theorem Prod.id_prod {α : Type u_1} {β : Type u_2} :
(fun p => (p.fst, p.snd)) = id
theorem Prod.map_id {α : Type u_1} {β : Type u_2} :
Prod.map id id = id
theorem Prod.fst_surjective {α : Type u_2} {β : Type u_1} [h : ] :
theorem Prod.snd_surjective {α : Type u_1} {β : Type u_2} [h : ] :
theorem Prod.fst_injective {α : Type u_2} {β : Type u_1} [inst : ] :
theorem Prod.snd_injective {α : Type u_1} {β : Type u_2} [inst : ] :
def Prod.swap {α : Type u_1} {β : Type u_2} :
α × ββ × α

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

Equations
• = (p.snd, p.fst)
@[simp]
theorem Prod.swap_swap {α : Type u_1} {β : Type u_2} (x : α × β) :
= x
@[simp]
theorem Prod.fst_swap {α : Type u_1} {β : Type u_2} {p : α × β} :
().fst = p.snd
@[simp]
theorem Prod.snd_swap {α : Type u_1} {β : Type u_2} {p : α × β} :
().snd = p.fst
@[simp]
theorem Prod.swap_prod_mk {α : Type u_1} {β : Type u_2} {a : α} {b : β} :
Prod.swap (a, b) = (b, a)
@[simp]
theorem Prod.swap_swap_eq {α : Type u_1} {β : Type u_2} :
Prod.swap Prod.swap = id
@[simp]
theorem Prod.swap_leftInverse {α : Type u_1} {β : Type u_2} :
Function.LeftInverse Prod.swap Prod.swap
@[simp]
theorem Prod.swap_rightInverse {α : Type u_1} {β : Type u_2} :
Function.RightInverse Prod.swap Prod.swap
theorem Prod.swap_injective {α : Type u_1} {β : Type u_2} :
theorem Prod.swap_surjective {α : Type u_1} {β : Type u_2} :
theorem Prod.swap_bijective {α : Type u_1} {β : Type u_2} :
@[simp]
theorem Prod.swap_inj {α : Type u_1} {β : Type u_2} {p : α × β} {q : α × β} :
p = q
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
theorem Prod.lex_iff {α : Type u_1} {β : Type u_2} {r : ααProp} {s : ββProp} {x : α × β} {y : α × β} :
Prod.Lex r s x y r x.fst y.fst x.fst = y.fst s x.snd y.snd
instance Prod.Lex.decidable {α : Type u_1} {β : Type u_2} [inst : ] (r : ααProp) (s : ββProp) [inst : ] [inst : ] :
Equations
theorem Prod.Lex.refl_left {α : Type u_1} {β : Type u_2} (r : ααProp) (s : ββProp) [inst : IsRefl α r] (x : α × β) :
Prod.Lex r s x x
instance Prod.instIsReflProdLex {α : Type u_1} {β : Type u_2} {r : ααProp} {s : ββProp} [inst : IsRefl α r] :
IsRefl (α × β) (Prod.Lex r s)
Equations
theorem Prod.Lex.refl_right {α : Type u_2} {β : Type u_1} (r : ααProp) (s : ββProp) [inst : IsRefl β s] (x : α × β) :
Prod.Lex r s x x
instance Prod.instIsReflProdLex_1 {α : Type u_1} {β : Type u_2} {r : ααProp} {s : ββProp} [inst : IsRefl β s] :
IsRefl (α × β) (Prod.Lex r s)
Equations
instance Prod.isIrrefl {α : Type u_1} {β : Type u_2} {r : ααProp} {s : ββProp} [inst : IsIrrefl α r] [inst : IsIrrefl β s] :
IsIrrefl (α × β) (Prod.Lex r s)
Equations
theorem Prod.Lex.trans {α : Type u_1} {β : Type u_2} {r : ααProp} {s : ββProp} [inst : IsTrans α r] [inst : IsTrans β s] {x : α × β} {y : α × β} {z : α × β} :
Prod.Lex r s x yProd.Lex r s y zProd.Lex r s x z
instance Prod.instIsTransProdLex {α : Type u_1} {β : Type u_2} {r : ααProp} {s : ββProp} [inst : IsTrans α r] [inst : IsTrans β s] :
IsTrans (α × β) (Prod.Lex r s)
Equations
instance Prod.instIsAntisymmProdLex {α : Type u_1} {β : Type u_2} {r : ααProp} {s : ββProp} [inst : ] [inst : ] :
IsAntisymm (α × β) (Prod.Lex r s)
Equations
instance Prod.isTotal_left {α : Type u_1} {β : Type u_2} {r : ααProp} {s : ββProp} [inst : IsTotal α r] :
IsTotal (α × β) (Prod.Lex r s)
Equations
instance Prod.isTotal_right {α : Type u_1} {β : Type u_2} {r : ααProp} {s : ββProp} [inst : ] [inst : IsTotal β s] :
IsTotal (α × β) (Prod.Lex r s)
Equations
instance Prod.IsTrichotomous {α : Type u_1} {β : Type u_2} {r : ααProp} {s : ββProp} [inst : ] [inst : ] :
IsTrichotomous (α × β) (Prod.Lex r s)
Equations
theorem Function.Injective.Prod_map {α : Type u_1} {β : Type u_3} {γ : Type u_2} {δ : Type u_4} {f : αγ} {g : βδ} (hf : ) (hg : ) :
theorem Function.Surjective.Prod_map {α : Type u_1} {β : Type u_3} {γ : Type u_2} {δ : Type u_4} {f : αγ} {g : βδ} (hf : ) (hg : ) :
theorem Function.Bijective.Prod_map {α : Type u_1} {β : Type u_3} {γ : Type u_2} {δ : Type u_4} {f : αγ} {g : βδ} (hf : ) (hg : ) :
theorem Function.LeftInverse.Prod_map {α : Type u_2} {β : Type u_1} {γ : Type u_4} {δ : Type u_3} {f₁ : αβ} {g₁ : γδ} {f₂ : βα} {g₂ : δγ} (hf : ) (hg : ) :
Function.LeftInverse (Prod.map f₁ g₁) (Prod.map f₂ g₂)
theorem Function.RightInverse.Prod_map {α : Type u_2} {β : Type u_1} {γ : Type u_4} {δ : Type u_3} {f₁ : αβ} {g₁ : γδ} {f₂ : βα} {g₂ : δγ} :
Function.RightInverse (Prod.map f₁ g₁) (Prod.map f₂ g₂)
theorem Function.Involutive.Prod_map {α : Type u_1} {β : Type u_2} {f : αα} {g : ββ} :
@[simp]
theorem Prod.map_injective {α : Type u_1} {β : Type u_2} {γ : Type u_4} {δ : Type u_3} [inst : ] [inst : ] {f : αγ} {g : βδ} :
@[simp]
theorem Prod.map_surjective {α : Type u_4} {β : Type u_3} {γ : Type u_1} {δ : Type u_2} [inst : ] [inst : ] {f : αγ} {g : βδ} :
@[simp]
theorem Prod.map_bijective {α : Type u_1} {β : Type u_2} {γ : Type u_4} {δ : Type u_3} [inst : ] [inst : ] {f : αγ} {g : βδ} :
@[simp]
theorem Prod.map_leftInverse {α : Type u_4} {β : Type u_1} {γ : Type u_3} {δ : Type u_2} [inst : ] [inst : ] {f₁ : αβ} {g₁ : γδ} {f₂ : βα} {g₂ : δγ} :
Function.LeftInverse (Prod.map f₁ g₁) (Prod.map f₂ g₂)
@[simp]
theorem Prod.map_rightInverse {α : Type u_1} {β : Type u_4} {γ : Type u_2} {δ : Type u_3} [inst : ] [inst : ] {f₁ : αβ} {g₁ : γδ} {f₂ : βα} {g₂ : δγ} :
Function.RightInverse (Prod.map f₁ g₁) (Prod.map f₂ g₂)
@[simp]
theorem Prod.map_involutive {α : Type u_1} {β : Type u_2} [inst : ] [inst : ] {f : αα} {g : ββ} :