# 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 : α × β} {y : β × α} :
x.swap = y ↔ x = y.swap
source
def Prod.mk.injArrow {α : Type u_1} {β : Type u_2} {x₁ : α} {y₁ : β} {x₂ : α} {y₂ : β} :
(x₁, y₁) = (x₂, y₂) → ⦃P : Sort u_5⦄ → (x₁ = x₂ → y₁ = y₂ → P) → P
Equations

- Prod.mk.injArrow h₁ h₂ = Prod.noConfusion h₁ h₂

Instances For

source
@[simp]
theorem Prod.mk.eta {α : Type u_1} {β : Type u_2} {p : α × β} :
(p.1, p.2) = p
source
theorem Prod.forall' {α : Type u_1} {β : Type u_2} {p : α → β → Prop} :
(∀ (x : α × β), p x.1 x.2) ↔ ∀ (a : α) (b : β), p a b
source
theorem Prod.exists' {α : Type u_1} {β : Type u_2} {p : α → β → Prop} :
(∃ (x : α × β), p x.1 x.2) ↔ ∃ (a : α), ∃ (b : β), p a b
source
@[simp]
theorem Prod.snd_comp_mk {α : Type u_1} {β : Type u_2} (x : α) :
snd ∘ mk x = id
source
@[simp]
theorem Prod.fst_comp_mk {α : Type u_1} {β : Type u_2} (x : α) :
fst ∘ mk x = Function.const β x
source
theorem Prod.map_apply' {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} (f : α → γ) (g : β → δ) (p : α × β) :
map f g p = (f p.1, g p.2)
source
theorem Prod.map_fst' {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} (f : α → γ) (g : β → δ) :
fst ∘ map f g = f ∘ fst
source
theorem Prod.map_snd' {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} (f : α → γ) (g : β → δ) :
snd ∘ map f g = g ∘ snd
source
theorem Prod.mk_inj {α : Type u_1} {β : Type u_2} {a₁ a₂ : α} {b₁ b₂ : β} :
(a₁, b₁) = (a₂, b₂) ↔ a₁ = a₂ ∧ b₁ = b₂
source
theorem Prod.mk_right_injective {α : Type u_5} {β : Type u_6} (a : α) :
Function.Injective (mk a)
source
theorem Prod.mk_left_injective {α : Type u_5} {β : Type u_6} (b : β) :
Function.Injective fun (a : α) => (a, b)
source
theorem Prod.mk_right_inj {α : Type u_1} {β : Type u_2} {a : α} {b₁ b₂ : β} :
(a, b₁) = (a, b₂) ↔ b₁ = b₂
source
theorem Prod.mk_left_inj {α : Type u_1} {β : Type u_2} {a₁ a₂ : α} {b : β} :
(a₁, b) = (a₂, b) ↔ a₁ = a₂
source
theorem Prod.map_def {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} {f : α → γ} {g : β → δ} :
map f g = fun (p : α × β) => (f p.1, g p.2)
source
theorem Prod.id_prod {α : Type u_1} {β : Type u_2} :
(fun (p : α × β) => (p.1, p.2)) = id
source
@[simp]
theorem Prod.map_iterate {α : Type u_1} {β : Type u_2} (f : α → α) (g : β → β) (n : ℕ) :
(map f g)^[n] = map f^[n] 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
@[simp]
theorem Prod.swap_leftInverse {α : Type u_1} {β : Type u_2} :
Function.LeftInverse swap swap
source
@[simp]
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 : α × β} :
p = q ↔ p.1 = q.1 ∧ p.2 = q.2
source
theorem Prod.fst_eq_iff {α : Type u_1} {β : Type u_2} {p : α × β} {x : α} :
p.1 = x ↔ p = (x, p.2)
source
theorem Prod.snd_eq_iff {α : Type u_1} {β : Type u_2} {p : α × β} {x : β} :
p.2 = x ↔ p = (p.1, x)
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.1 y.1 ∨ x.1 = y.1 ∧ s x.2 y.2
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

- Prod.Lex.decidable r s x✝¹ x✝ = decidable_of_decidable_of_iff ⋯

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.instIsReflLex {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop} [IsRefl α r] :
IsRefl (α × β) (Prod.Lex r s)
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.instIsReflLex_1 {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop} [IsRefl β s] :
IsRefl (α × β) (Prod.Lex r s)
source
instance Prod.isIrrefl {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop} [IsIrrefl α r] [IsIrrefl β s] :
IsIrrefl (α × β) (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.Lex r s x y → Prod.Lex r s y z → Prod.Lex r s x z
source
instance Prod.instIsTransLex {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop} [IsTrans α r] [IsTrans β s] :
IsTrans (α × β) (Prod.Lex r s)
source
instance Prod.instIsAntisymmLexOfIsStrictOrder {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop} [IsStrictOrder α r] [IsAntisymm β s] :
IsAntisymm (α × β) (Prod.Lex r s)
source
instance Prod.isTotal_left {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop} [IsTotal α r] :
IsTotal (α × β) (Prod.Lex r s)
source
instance Prod.isTotal_right {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop} [_root_.IsTrichotomous α r] [IsTotal β s] :
IsTotal (α × β) (Prod.Lex r s)
source
instance Prod.IsTrichotomous {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop} [_root_.IsTrichotomous α r] [_root_.IsTrichotomous β s] :
_root_.IsTrichotomous (α × β) (Prod.Lex r s)
source
instance Prod.instIsAsymmLex {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop} [IsAsymm α r] [IsAsymm β s] :
IsAsymm (α × β) (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
@[simp]
theorem Prod.map_injective {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} [Nonempty α] [Nonempty β] {f : α → γ} {g : β → δ} :
Function.Injective (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 (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 (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 (map f₁ g₁) (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 (map f₁ g₁) (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 (map f g) ↔ Function.Involutive f ∧ Function.Involutive g
source
opaque Prod.PrettyPrinting.pp.numericProj.prod :
Lean.Option Bool

When true, then `Prod.fst x` and `Prod.snd x` pretty print as `x.1` and `x.2` rather than as `x.fst` and `x.snd`.

source
def Prod.PrettyPrinting.getPPNumericProjProd (o : Lean.Options) :
Bool

Tell whether pretty-printing should use numeric projection notations `.1` and `.2` for `Prod.fst` and `Prod.snd`.

Equations

- Prod.PrettyPrinting.getPPNumericProjProd o = Lean.KVMap.get o Prod.PrettyPrinting.pp.numericProj.prod.name Prod.PrettyPrinting.pp.numericProj.prod.defValue

Instances For

source
def Prod.PrettyPrinting.delabProdFst :
Lean.PrettyPrinter.Delaborator.Delab

Delaborator for `Prod.fst x` as `x.1`.

Equations

- One or more equations did not get rendered due to their size.

Instances For

source
def Prod.PrettyPrinting.delabProdSnd :
Lean.PrettyPrinter.Delaborator.Delab

Delaborator for `Prod.snd x` as `x.2`.

Equations

- One or more equations did not get rendered due to their size.

Instances For