Extra facts about Prod

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

theorem Prod.swap_eq_iff_eq_swap {α : Type u_1} {β : Type u_2} {x : α × β} {y : β × α} : x.swap = y ↔ x = y.swap

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

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

@[simp]

theorem Prod.mk.eta {α : Type u_1} {β : Type u_2} {p : α × β} : (p.1, p.2) = p

theorem Prod.forall' {α : Type u_1} {β : Type u_2} {p : α → β → Prop} : (∀ (x : α × β), p x.1 x.2) ↔ ∀ (a : α) (b : β), p a b

theorem Prod.exists' {α : Type u_1} {β : Type u_2} {p : α → β → Prop} : (∃ (x : α × β), p x.1 x.2) ↔ ∃ (a : α), ∃ (b : β), p a b

@[simp]

theorem Prod.snd_comp_mk {α : Type u_1} {β : Type u_2} (x : α) : snd ∘ mk x = id

@[simp]

theorem Prod.fst_comp_mk {α : Type u_1} {β : Type u_2} (x : α) : fst ∘ mk x = Function.const β x

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)

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

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

theorem Prod.mk_inj {α : Type u_1} {β : Type u_2} {a₁ a₂ : α} {b₁ b₂ : β} : (a₁, b₁) = (a₂, b₂) ↔ a₁ = a₂ ∧ b₁ = b₂

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

theorem Prod.mk_left_injective {α : Type u_5} {β : Type u_6} (b : β) : Function.Injective fun (a : α) => (a, b)

theorem Prod.mk_right_inj {α : Type u_1} {β : Type u_2} {a : α} {b₁ b₂ : β} : (a, b₁) = (a, b₂) ↔ b₁ = b₂

theorem Prod.mk_left_inj {α : Type u_1} {β : Type u_2} {a₁ a₂ : α} {b : β} : (a₁, b) = (a₂, b) ↔ a₁ = a₂

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)

theorem Prod.id_prod {α : Type u_1} {β : Type u_2} : (fun (p : α × β) => (p.1, p.2)) = id

@[simp]

theorem Prod.map_iterate {α : Type u_1} {β : Type u_2} (f : α → α) (g : β → β) (n : ℕ) : (map f g)^[n] = map f^[n] g^[n]

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

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

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

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

@[simp]

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

@[simp]

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

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

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

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

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

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

theorem Prod.fst_eq_iff {α : Type u_1} {β : Type u_2} {p : α × β} {x : α} : p.1 = x ↔ p = (x, p.2)

theorem Prod.snd_eq_iff {α : Type u_1} {β : Type u_2} {p : α × β} {x : β} : p.2 = x ↔ p = (p.1, x)

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

@[instance_reducible]

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 ⋯

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

instance Prod.instReflLex_mathlib {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop} [Std.Refl r] : Std.Refl (Prod.Lex r s)

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

instance Prod.instReflLex_mathlib_1 {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop} [Std.Refl s] : Std.Refl (Prod.Lex r s)

instance Prod.instIrreflLex_mathlib {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop} [Std.Irrefl r] [Std.Irrefl s] : Std.Irrefl (Prod.Lex r s)

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

instance Prod.instIsTransLex {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop} [IsTrans α r] [IsTrans β s] : IsTrans (α × β) (Prod.Lex r s)

instance Prod.instAntisymmLexOfIsStrictOrder {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop} [IsStrictOrder α r] [Std.Antisymm s] : Std.Antisymm (Prod.Lex r s)

instance Prod.total_left {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop} [Std.Total r] : Std.Total (Prod.Lex r s)

instance Prod.total_right {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop} [Std.Trichotomous r] [Std.Total s] : Std.Total (Prod.Lex r s)

instance Prod.trichotomous {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop} [Std.Trichotomous r] [Std.Trichotomous s] : Std.Trichotomous (Prod.Lex r s)

instance Prod.instAsymmLex_mathlib {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop} [Std.Asymm r] [Std.Asymm s] : Std.Asymm (Prod.Lex r s)

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)

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)

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)

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₂)

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₂)

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

@[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

@[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

@[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

@[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₂

@[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₂

@[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

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.

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 = o.get Prod.PrettyPrinting.pp.numericProj.prod.name Prod.PrettyPrinting.pp.numericProj.prod.defValue

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.

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.