mathlib3 documentation

data.prod.basic

Extra facts about prod #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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.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
@[simp]
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_1} {β : Type u_2} (a : α) :
function.injective (prod.mk a)
source
theorem prod.mk.inj_right {α : Type u_1} {β : Type u_2} (b : β) :
function.injective (λ (a : α), (a, b))
source
theorem prod.mk_inj_left {α : Type u_1} {β : Type u_2} {a : α} {b₁ b₂ : β} :
(a, b₁) = (a, b₂) ↔ b₁ = b₂
source
theorem prod.mk_inj_right {α : Type u_1} {β : Type u_2} {a₁ a₂ : α} {b : β} :
(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
@[ext]
theorem prod.ext {α : Type u_1} {β : Type u_2} {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 = λ (p : α × β), (f p.fst, g p.snd)
source
theorem prod.id_prod {α : Type u_1} {β : Type u_2} :
(λ (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
source
@[simp]
theorem prod.swap_swap {α : Type u_1} {β : Type u_2} (x : α × β) :
x.swap.swap = x
source
@[simp]
theorem prod.fst_swap {α : Type u_1} {β : Type u_2} {p : α × β} :
p.swap.fst = p.snd
source
@[simp]
theorem prod.snd_swap {α : Type u_1} {β : Type u_2} {p : α × β} :
p.swap.snd = p.fst
source
@[simp]
theorem prod.swap_prod_mk {α : Type u_1} {β : Type u_2} {a : α} {b : β} :
(a, b).swap = (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_left_inverse {α : Type u_1} {β : Type u_2} :
function.left_inverse prod.swap prod.swap
source
@[simp]
theorem prod.swap_right_inverse {α : Type u_1} {β : Type u_2} :
function.right_inverse 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 : α × β} :
p.swap = q.swap ↔ 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
@[protected, 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
source
@[refl]
theorem prod.lex.refl_left {α : Type u_1} {β : Type u_2} (r : α → α → Prop) (s : β → β → Prop) [is_refl α r] (x : α × β) :
prod.lex r s x x
source
@[protected, instance]
def prod.is_refl_left {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop} [is_refl α r] :
is_refl (α × β) (prod.lex r s)
source
@[refl]
theorem prod.lex.refl_right {α : Type u_1} {β : Type u_2} (r : α → α → Prop) (s : β → β → Prop) [is_refl β s] (x : α × β) :
prod.lex r s x x
source
@[protected, instance]
def prod.is_refl_right {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop} [is_refl β s] :
is_refl (α × β) (prod.lex r s)
source
@[protected, instance]
def prod.is_irrefl {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop} [is_irrefl α r] [is_irrefl β s] :
is_irrefl (α × β) (prod.lex r s)
source
@[trans]
theorem prod.lex.trans {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop} [is_trans α r] [is_trans β s] {x y z : α × β} :
prod.lex r s x y → prod.lex r s y z → prod.lex r s x z
source
@[protected, instance]
def prod.lex.is_trans {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop} [is_trans α r] [is_trans β s] :
is_trans (α × β) (prod.lex r s)
source
@[protected, instance]
def prod.lex.is_antisymm {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop} [is_strict_order α r] [is_antisymm β s] :
is_antisymm (α × β) (prod.lex r s)
source
@[protected, instance]
def prod.is_total_left {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop} [is_total α r] :
is_total (α × β) (prod.lex r s)
source
@[protected, instance]
def prod.is_total_right {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop} [is_trichotomous α r] [is_total β s] :
is_total (α × β) (prod.lex r s)
source
@[protected, instance]
def prod.is_trichotomous {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop} [is_trichotomous α r] [is_trichotomous β s] :
is_trichotomous (α × β) (prod.lex r s)
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.left_inverse.prod_map {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} {f₁ : α → β} {g₁ : γ → δ} {f₂ : β → α} {g₂ : δ → γ} (hf : function.left_inverse f₁ f₂) (hg : function.left_inverse g₁ g₂) :
function.left_inverse (prod.map f₁ g₁) (prod.map f₂ g₂)
source
theorem function.right_inverse.prod_map {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} {f₁ : α → β} {g₁ : γ → δ} {f₂ : β → α} {g₂ : δ → γ} :
function.right_inverse f₁ f₂ → function.right_inverse g₁ g₂ → function.right_inverse (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_left_inverse {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} [nonempty β] [nonempty δ] {f₁ : α → β} {g₁ : γ → δ} {f₂ : β → α} {g₂ : δ → γ} :
function.left_inverse (prod.map f₁ g₁) (prod.map f₂ g₂) ↔ function.left_inverse f₁ f₂ ∧ function.left_inverse g₁ g₂
source
@[simp]
theorem prod.map_right_inverse {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} [nonempty α] [nonempty γ] {f₁ : α → β} {g₁ : γ → δ} {f₂ : β → α} {g₂ : δ → γ} :
function.right_inverse (prod.map f₁ g₁) (prod.map f₂ g₂) ↔ function.right_inverse f₁ f₂ ∧ function.right_inverse 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