Extra facts about `Prod` #

This file proves various simple lemmas about Prod. It also defines better delaborators for product projections.

source

theorem Prod.swap_eq_iff_eq_swap {α : Type u_1} {β : Type u_2} {x : Prod α β} {y : Prod β α} :

Iff (Eq x.swap y) (Eq x y.swap)

source

def Prod.mk.injArrow {α : Type u_1} {β : Type u_2} {x₁ : α} {y₁ : β} {x₂ : α} {y₂ : β} :

Eq { fst := x₁, snd := y₁ } { fst := x₂, snd := y₂ } → ⦃P : Sort u_5⦄ → (Eq x₁ x₂ → Eq y₁ y₂ → P) → P

Equations

Eq (Prod.mk.injArrow h₁ h₂) (Prod.noConfusion h₁ h₂)

Instances For

source

theorem Prod.mk.eta {α : Type u_1} {β : Type u_2} {p : Prod α β} :

Eq { fst := p.fst, snd := p.snd } p

source

theorem Prod.forall' {α : Type u_1} {β : Type u_2} {p : α → β → Prop} :

Iff (∀ (x : Prod α β), p x.fst x.snd) (∀ (a : α) (b : β), p a b)

source

theorem Prod.exists' {α : Type u_1} {β : Type u_2} {p : α → β → Prop} :

Iff (Exists fun (x : Prod α β) => p x.fst x.snd) (Exists fun (a : α) => Exists fun (b : β) => p a b)

source

theorem Prod.snd_comp_mk {α : Type u_1} {β : Type u_2} (x : α) :

Eq (Function.comp snd (mk x)) id

source

theorem Prod.fst_comp_mk {α : Type u_1} {β : Type u_2} (x : α) :

Eq (Function.comp fst (mk x)) (Function.const β x)

source

@[deprecated Prod.map_apply (since := "2024-10-17")]

theorem Prod.map_mk {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} (f : α → β) (g : γ → δ) (x : α) (y : γ) :

Eq (map f g { fst := x, snd := y }) { fst := f x, snd := g y }

Alias of Prod.map_apply.

source

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

Eq (map f g p) { fst := f p.fst, snd := g p.snd }

source

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

Eq (Function.comp fst (map f g)) (Function.comp f fst)

source

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

Eq (Function.comp snd (map f g)) (Function.comp g snd)

source

theorem Prod.mk_inj {α : Type u_1} {β : Type u_2} {a₁ a₂ : α} {b₁ b₂ : β} :

Iff (Eq { fst := a₁, snd := b₁ } { fst := a₂, snd := b₂ }) (And (Eq a₁ a₂) (Eq b₁ b₂))

source

@[deprecated Prod.mk_inj (since := "2025-03-06")]

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

Iff (Eq { fst := a₁, snd := b₁ } { fst := a₂, snd := b₂ }) (And (Eq a₁ a₂) (Eq b₁ b₂))

Alias of Prod.mk_inj.

source

theorem Prod.mk_right_injective {α : Type u_5} {β : Type u_6} (a : α) :

Function.Injective (mk a)

source

@[deprecated Prod.mk_right_injective (since := "2025-03-06")]

theorem Prod.mk.inj_left {α : Type u_5} {β : Type u_6} (a : α) :

Function.Injective (mk a)

Alias of Prod.mk_right_injective.

source

theorem Prod.mk_left_injective {α : Type u_5} {β : Type u_6} (b : β) :

Function.Injective fun (a : α) => { fst := a, snd := b }

source

@[deprecated Prod.mk_left_injective (since := "2025-03-06")]

theorem Prod.mk.inj_right {α : Type u_5} {β : Type u_6} (b : β) :

Function.Injective fun (a : α) => { fst := a, snd := b }

Alias of Prod.mk_left_injective.

source

theorem Prod.mk_right_inj {α : Type u_1} {β : Type u_2} {a : α} {b₁ b₂ : β} :

Iff (Eq { fst := a, snd := b₁ } { fst := a, snd := b₂ }) (Eq b₁ b₂)

source

theorem Prod.mk_left_inj {α : Type u_1} {β : Type u_2} {a₁ a₂ : α} {b : β} :

Iff (Eq { fst := a₁, snd := b } { fst := a₂, snd := b }) (Eq a₁ a₂)

source

@[deprecated Prod.mk_right_inj (since := "2025-03-06")]

theorem Prod.mk_inj_left {α : Type u_1} {β : Type u_2} {a : α} {b₁ b₂ : β} :

Iff (Eq { fst := a, snd := b₁ } { fst := a, snd := b₂ }) (Eq b₁ b₂)

Alias of Prod.mk_right_inj.

source

@[deprecated Prod.mk_left_inj (since := "2025-03-06")]

theorem Prod.mk_inj_right {α : Type u_1} {β : Type u_2} {a₁ a₂ : α} {b : β} :

Iff (Eq { fst := a₁, snd := b } { fst := a₂, snd := b }) (Eq a₁ a₂)

Alias of Prod.mk_left_inj.

source

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

Eq (map f g) fun (p : Prod α β) => { fst := f p.fst, snd := g p.snd }

source

theorem Prod.id_prod {α : Type u_1} {β : Type u_2} :

Eq (fun (p : Prod α β) => { fst := p.fst, snd := p.snd }) id

source

theorem Prod.map_iterate {α : Type u_1} {β : Type u_2} (f : α → α) (g : β → β) (n : Nat) :

Eq (Nat.iterate (map f g) n) (map (Nat.iterate f n) (Nat.iterate g n))

source

theorem Prod.fst_surjective {α : Type u_1} {β : Type u_2} [h : Nonempty β] :

Function.Surjective fst

source

theorem Prod.snd_surjective {α : Type u_1} {β : Type u_2} [h : Nonempty α] :

Function.Surjective snd

source

theorem Prod.fst_injective {α : Type u_1} {β : Type u_2} [Subsingleton β] :

Function.Injective fst

source

theorem Prod.snd_injective {α : Type u_1} {β : Type u_2} [Subsingleton α] :

Function.Injective snd

source

theorem Prod.swap_leftInverse {α : Type u_1} {β : Type u_2} :

Function.LeftInverse swap swap

source

theorem Prod.swap_rightInverse {α : Type u_1} {β : Type u_2} :

Function.RightInverse swap swap

source

theorem Prod.swap_injective {α : Type u_1} {β : Type u_2} :

Function.Injective swap

source

theorem Prod.swap_surjective {α : Type u_1} {β : Type u_2} :

Function.Surjective swap

source

theorem Prod.swap_bijective {α : Type u_1} {β : Type u_2} :

Function.Bijective swap

source

theorem Function.Semiconj.swap_map {α : Type u_1} {β : Type u_2} (f : α → α) (g : β → β) :

Semiconj Prod.swap (Prod.map f g) (Prod.map g f)

source

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

Iff (Eq p q) (And (Eq p.fst q.fst) (Eq p.snd q.snd))

source

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

Iff (Eq p.fst x) (Eq p { fst := x, snd := p.snd })

source

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

Iff (Eq p.snd x) (Eq p { fst := p.fst, snd := x })

source

theorem Prod.lex_iff {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop} {x y : Prod α β} :

Iff (Prod.Lex r s x y) (Or (r x.fst y.fst) (And (Eq x.fst y.fst) (s x.snd y.snd)))

source

def Prod.Lex.decidable {α : Type u_1} {β : Type u_2} [DecidableEq α] (r : α → α → Prop) (s : β → β → Prop) [DecidableRel r] [DecidableRel s] :

DecidableRel (Prod.Lex r s)

Equations

Eq (Prod.Lex.decidable r s x✝¹ x✝) (decidable_of_decidable_of_iff ⋯)

Instances For

source

theorem Prod.Lex.refl_left {α : Type u_1} {β : Type u_2} (r : α → α → Prop) (s : β → β → Prop) [IsRefl α r] (x : Prod α β) :

Prod.Lex r s x x

source

theorem Prod.instIsReflLex {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop} [IsRefl α r] :

IsRefl (Prod α β) (Prod.Lex r s)

source

theorem Prod.Lex.refl_right {α : Type u_1} {β : Type u_2} (r : α → α → Prop) (s : β → β → Prop) [IsRefl β s] (x : Prod α β) :

Prod.Lex r s x x

source

theorem Prod.instIsReflLex_1 {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop} [IsRefl β s] :

IsRefl (Prod α β) (Prod.Lex r s)

source

theorem Prod.isIrrefl {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop} [IsIrrefl α r] [IsIrrefl β s] :

IsIrrefl (Prod α β) (Prod.Lex r s)

source

theorem Prod.Lex.trans {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop} [IsTrans α r] [IsTrans β s] {x y z : Prod α β} :

Prod.Lex r s x y → Prod.Lex r s y z → Prod.Lex r s x z

source

theorem Prod.instIsTransLex {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop} [IsTrans α r] [IsTrans β s] :

IsTrans (Prod α β) (Prod.Lex r s)

source

theorem Prod.instIsAntisymmLexOfIsStrictOrder {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop} [IsStrictOrder α r] [IsAntisymm β s] :

IsAntisymm (Prod α β) (Prod.Lex r s)

source

theorem Prod.isTotal_left {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop} [IsTotal α r] :

IsTotal (Prod α β) (Prod.Lex r s)

source

theorem Prod.isTotal_right {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop} [_root_.IsTrichotomous α r] [IsTotal β s] :

IsTotal (Prod α β) (Prod.Lex r s)

source

theorem Prod.IsTrichotomous {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop} [_root_.IsTrichotomous α r] [_root_.IsTrichotomous β s] :

_root_.IsTrichotomous (Prod α β) (Prod.Lex r s)

source

theorem Prod.instIsAsymmLex {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop} [IsAsymm α r] [IsAsymm β s] :

IsAsymm (Prod α β) (Prod.Lex r s)

source

theorem Function.Injective.prodMap {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} {f : α → γ} {g : β → δ} (hf : Injective f) (hg : Injective g) :

Injective (Prod.map f g)

source

theorem Function.Surjective.prodMap {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} {f : α → γ} {g : β → δ} (hf : Surjective f) (hg : Surjective g) :

Surjective (Prod.map f g)

source

theorem Function.Bijective.prodMap {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} {f : α → γ} {g : β → δ} (hf : Bijective f) (hg : Bijective g) :

Bijective (Prod.map f g)

source

theorem Function.LeftInverse.prodMap {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} {f₁ : α → β} {g₁ : γ → δ} {f₂ : β → α} {g₂ : δ → γ} (hf : LeftInverse f₁ f₂) (hg : LeftInverse g₁ g₂) :

LeftInverse (Prod.map f₁ g₁) (Prod.map f₂ g₂)

source

theorem Function.RightInverse.prodMap {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} {f₁ : α → β} {g₁ : γ → δ} {f₂ : β → α} {g₂ : δ → γ} :

RightInverse f₁ f₂ → RightInverse g₁ g₂ → RightInverse (Prod.map f₁ g₁) (Prod.map f₂ g₂)

source

theorem Function.Involutive.prodMap {α : Type u_1} {β : Type u_2} {f : α → α} {g : β → β} :

Involutive f → Involutive g → Involutive (Prod.map f g)

source

theorem Prod.map_injective {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} [Nonempty α] [Nonempty β] {f : α → γ} {g : β → δ} :

Iff (Function.Injective (map f g)) (And (Function.Injective f) (Function.Injective g))

source

theorem Prod.map_surjective {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} [Nonempty γ] [Nonempty δ] {f : α → γ} {g : β → δ} :

Iff (Function.Surjective (map f g)) (And (Function.Surjective f) (Function.Surjective g))

source

theorem Prod.map_bijective {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} [Nonempty α] [Nonempty β] {f : α → γ} {g : β → δ} :

Iff (Function.Bijective (map f g)) (And (Function.Bijective f) (Function.Bijective g))

source

theorem Prod.map_leftInverse {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} [Nonempty β] [Nonempty δ] {f₁ : α → β} {g₁ : γ → δ} {f₂ : β → α} {g₂ : δ → γ} :

Iff (Function.LeftInverse (map f₁ g₁) (map f₂ g₂)) (And (Function.LeftInverse f₁ f₂) (Function.LeftInverse g₁ g₂))

source

theorem Prod.map_rightInverse {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} [Nonempty α] [Nonempty γ] {f₁ : α → β} {g₁ : γ → δ} {f₂ : β → α} {g₂ : δ → γ} :