Documentation

Mathlib.Data.Prod.Basic

Extra facts about Prod #

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

source
@[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)
source
@[simp]
theorem Prod.mk.eta {α : Type u_1} {β : Type u_2} {p : α × β} :
(p.fst, p.snd) = p
source
@[simp]
theorem Prod.forall {α : Type u_1} {β : Type u_2} {p : α × β → Prop} :
((x : α × β) → p x) ↔ (a : α) → (b : β) → p (a, b)
source
@[simp]
theorem Prod.exists {α : Type u_1} {β : Type u_2} {p : α × β → Prop} :
(∃ x, p x) ↔ ∃ a b, p (a, b)
source
theorem Prod.forall' {α : Type u_1} {β : Type u_2} {p : α → β → Prop} :
((x : α × β) → p x.fst x.snd) ↔ (a : α) → (b : β) → p a b
source
theorem Prod.exists' {α : Type u_1} {β : Type u_2} {p : α → β → Prop} :
(∃ x, p x.fst x.snd) ↔ ∃ a b, p a b
source
@[simp]
theorem Prod.snd_comp_mk {α : Type u_1} {β : Type u_2} (x : α) :
Prod.snd ∘ Prod.mk x = id
source
@[simp]
theorem Prod.fst_comp_mk {α : Type u_1} {β : Type u_2} (x : α) :
Prod.fst ∘ Prod.mk x = Function.const β x
source
@[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)
source
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
source
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
source
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
source
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
source
theorem Prod.map_comp_map {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} {ε : Type u_5} {ζ : Type u_6} (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.

source
theorem Prod.map_map {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} {ε : Type u_5} {ζ : Type u_6} (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.

source
theorem Prod.mk.inj_iff {α : Type u_1} {β : Type u_2} {a₁ : α} {a₂ : α} {b₁ : β} {b₂ : β} :
(a₁, b₁) = (a₂, b₂) ↔ a₁ = a₂ ∧ b₁ = b₂
source
theorem Prod.mk.inj_left {α : Type u_5} {β : Type u_6} (a : α) :
Function.Injective (Prod.mk a)
source
theorem Prod.mk.inj_right {α : Type u_5} {β : Type u_6} (b : β) :
Function.Injective fun a => (a, b)
source
theorem Prod.mk_inj_left :
∀ {α : Type u_5} {a : α} {β : Type u_6} {b₁ b₂ : β}, (a, b₁) = (a, b₂) ↔ b₁ = b₂
source
theorem Prod.mk_inj_right :
∀ {α : Type u_5} {a₁ : α} {β : Type u_6} {b : β} {a₂ : α}, (a₁, b) = (a₂, b) ↔ a₁ = a₂
source
theorem Prod.ext_iff {α : Type u_1} {β : Type u_2} {p : α × β} {q : α × β} :
p = q ↔ p.fst = q.fst ∧ p.snd = q.snd
source
theorem Prod.ext {α : Type u_5} {β : Type u_6} {p : α × β} {q : α × β} (h₁ : p.fst = q.fst) (h₂ : p.snd = q.snd) :
p = q
source
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)
source
theorem Prod.id_prod {α : Type u_1} {β : Type u_2} :
(fun p => (p.fst, p.snd)) = id
source
@[simp]
theorem Prod.map_id {α : Type u_1} {β : Type u_2} :
Prod.map id id = id
source
theorem Prod.fst_surjective {α : Type u_1} {β : Type u_2} [h : Nonempty β] :
Function.Surjective Prod.fst
source
theorem Prod.snd_surjective {α : Type u_1} {β : Type u_2} [h : Nonempty α] :
Function.Surjective Prod.snd
source
theorem Prod.fst_injective {α : Type u_1} {β : Type u_2} [Subsingleton β] :
Function.Injective Prod.fst
source
theorem Prod.snd_injective {α : Type u_1} {β : Type u_2} [Subsingleton α] :
Function.Injective Prod.snd
source
def Prod.swap {α : Type u_1} {β : Type u_2} :
α × β → β × α

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

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