doc-next-gen

Mathlib.Data.Prod.Basic

Module docstring

{"# Extra facts about Prod

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

Prod.swap_eq_iff_eq_swap theorem
{x : α × β} {y : β × α} : x.swap = y ↔ x = y.swap
Full source 
lemma swap_eq_iff_eq_swap {x : α × β} {y : β × α} : x.swap = y ↔ x = y.swap := by aesop
Equivalence of Pair Swapping: $x.\text{swap} = y \leftrightarrow x = y.\text{swap}$
Informal description
For any pairs $x \in \alpha \times \beta$ and $y \in \beta \times \alpha$, the swap of $x$ equals $y$ if and only if $x$ equals the swap of $y$. In other words, $x.\text{swap} = y \leftrightarrow x = y.\text{swap}$.
Prod.mk.injArrow definition
{x₁ : α} {y₁ : β} {x₂ : α} {y₂ : β} : (x₁, y₁) = (x₂, y₂) → ∀ ⦃P : Sort*⦄, (x₁ = x₂ → y₁ = y₂ → P) → P
Full source 
def mk.injArrow {x₁ : α} {y₁ : β} {x₂ : α} {y₂ : β} :
    (x₁, y₁) = (x₂, y₂) → ∀ ⦃P : Sort*⦄, (x₁ = x₂ → y₁ = y₂ → P) → P :=
  fun h₁ _ h₂ ↦ Prod.noConfusion h₁ h₂
Equality of pairs implies equality of components
Informal description
For any elements \( x_1, x_2 \in \alpha \) and \( y_1, y_2 \in \beta \), if the pairs \( (x_1, y_1) \) and \( (x_2, y_2) \) are equal, then for any proposition \( P \), the implication \( (x_1 = x_2 \to y_1 = y_2 \to P) \) implies \( P \).
Prod.mk.eta theorem
: ∀ {p : α × β}, (p.1, p.2) = p
Full source 
@[simp]
theorem mk.eta : ∀ {p : α × β}, (p.1, p.2) = p
  | (_, _) => rfl
Eta Reduction for Product Pairs
Informal description
For any pair $p = (a, b)$ in the product type $\alpha \times \beta$, the pair $(p.1, p.2)$ is equal to $p$ itself.
Prod.forall' theorem
{p : α → β → Prop} : (∀ x : α × β, p x.1 x.2) ↔ ∀ a b, p a b
Full source 
theorem forall' {p : α → β → Prop} : (∀ x : α × β, p x.1 x.2) ↔ ∀ a b, p a b :=
  Prod.forall
Universal Quantification over Product Types
Informal description
For any predicate $p : \alpha \to \beta \to \text{Prop}$, the following are equivalent: 1. For all pairs $(a, b) \in \alpha \times \beta$, the proposition $p\,a\,b$ holds. 2. For all elements $a \in \alpha$ and $b \in \beta$, the proposition $p\,a\,b$ holds.
Prod.exists' theorem
{p : α → β → Prop} : (∃ x : α × β, p x.1 x.2) ↔ ∃ a b, p a b
Full source 
theorem exists' {p : α → β → Prop} : (∃ x : α × β, p x.1 x.2) ↔ ∃ a b, p a b :=
  Prod.exists
Existence in Product Type is Equivalent to Component-wise Existence
Informal description
For any predicate $p : \alpha \to \beta \to \text{Prop}$, there exists a pair $(x_1, x_2) \in \alpha \times \beta$ such that $p(x_1, x_2)$ holds if and only if there exist elements $a \in \alpha$ and $b \in \beta$ such that $p(a, b)$ holds.
Prod.snd_comp_mk theorem
(x : α) : Prod.snd ∘ (Prod.mk x : β → α × β) = id
Full source 
@[simp]
theorem snd_comp_mk (x : α) : Prod.sndProd.snd ∘ (Prod.mk x : β → α × β) = id :=
  rfl
Second Projection Composed with Pair Construction is Identity
Informal description
For any element $x$ of type $\alpha$, the composition of the second projection function $\mathrm{snd}$ with the function $\mathrm{mk}\ x$ (which maps an element of $\beta$ to the pair $(x, \cdot)$) is equal to the identity function on $\beta$.
Prod.fst_comp_mk theorem
(x : α) : Prod.fst ∘ (Prod.mk x : β → α × β) = Function.const β x
Full source 
@[simp]
theorem fst_comp_mk (x : α) : Prod.fstProd.fst ∘ (Prod.mk x : β → α × β) = Function.const β x :=
  rfl
First Projection of Constant Pair Construction is Constant Function
Informal description
For any element $x$ of type $\alpha$, the composition of the first projection function $\mathrm{fst}$ with the function $\mathrm{mk}_x : \beta \to \alpha \times \beta$ (which maps $y \mapsto (x, y)$) is equal to the constant function on $\beta$ that always returns $x$.
Prod.map_apply' theorem
(f : α → γ) (g : β → δ) (p : α × β) : map f g p = (f p.1, g p.2)
Full source 
theorem map_apply' (f : α → γ) (g : β → δ) (p : α × β) : map f g p = (f p.1, g p.2) :=
  rfl
Mapping a Pair Component-wise: $\mathrm{map}\ f\ g\ (a, b) = (f(a), g(b))$
Informal description
For any functions $f \colon \alpha \to \gamma$ and $g \colon \beta \to \delta$, and any pair $p = (a, b) \in \alpha \times \beta$, the mapped pair $\mathrm{map}\ f\ g\ p$ is equal to $(f(a), g(b))$.
Prod.map_fst' theorem
(f : α → γ) (g : β → δ) : Prod.fst ∘ map f g = f ∘ Prod.fst
Full source 
theorem map_fst' (f : α → γ) (g : β → δ) : Prod.fstProd.fst ∘ map f g = f ∘ Prod.fst :=
  funext <| map_fst f g
First Projection Commutes with Product Map
Informal description
For any functions $f : \alpha \to \gamma$ and $g : \beta \to \delta$, the composition of the first projection function $\mathrm{fst}$ with the product map $\mathrm{map}\,f\,g$ is equal to the composition of $f$ with $\mathrm{fst}$. In other words, $\mathrm{fst} \circ (\mathrm{map}\,f\,g) = f \circ \mathrm{fst}$.
Prod.map_snd' theorem
(f : α → γ) (g : β → δ) : Prod.snd ∘ map f g = g ∘ Prod.snd
Full source 
theorem map_snd' (f : α → γ) (g : β → δ) : Prod.sndProd.snd ∘ map f g = g ∘ Prod.snd :=
  funext <| map_snd f g
Second Projection Commutes with Product Map
Informal description
For any functions $f \colon \alpha \to \gamma$ and $g \colon \beta \to \delta$, the composition of the second projection with the product map $(f, g)$ is equal to the composition of $g$ with the second projection. In symbols: \[ \text{snd} \circ \text{map}\, f\, g = g \circ \text{snd} \]
Prod.mk_inj theorem
{a₁ a₂ : α} {b₁ b₂ : β} : (a₁, b₁) = (a₂, b₂) ↔ a₁ = a₂ ∧ b₁ = b₂
Full source 
theorem mk_inj {a₁ a₂ : α} {b₁ b₂ : β} : (a₁, b₁)(a₁, b₁) = (a₂, b₂) ↔ a₁ = a₂ ∧ b₁ = b₂ := by simp
Pair Equality Criterion: $(a₁, b₁) = (a₂, b₂) ↔ a₁ = a₂ ∧ b₁ = b₂$
Informal description
For any elements $a₁, a₂$ in type $\alpha$ and $b₁, b₂$ in type $\beta$, the pair $(a₁, b₁)$ equals $(a₂, b₂)$ if and only if $a₁ = a₂$ and $b₁ = b₂$.
Prod.mk_right_injective theorem
{α β : Type*} (a : α) : (mk a : β → α × β).Injective
Full source 
theorem mk_right_injective {α β : Type*} (a : α) : (mk a : β → α × β).Injective := by
  intro b₁ b₂ h
  simpa only [true_and, Prod.mk_inj, eq_self_iff_true] using h
Injectivity of Right Pair Construction with Fixed First Component
Informal description
For any fixed element $a$ in type $\alpha$, the function that maps an element $b$ in type $\beta$ to the pair $(a, b)$ is injective. In other words, if $(a, b_1) = (a, b_2)$, then $b_1 = b_2$.
Prod.mk_left_injective theorem
{α β : Type*} (b : β) : (fun a ↦ mk a b : α → α × β).Injective
Full source 
theorem mk_left_injective {α β : Type*} (b : β) : (fun a ↦ mk a b : α → α × β).Injective := by
  intro b₁ b₂ h
  simpa only [and_true, eq_self_iff_true, mk_inj] using h
Injectivity of Left Projection in Product Type: $(a, b) \mapsto a$ is injective for fixed $b$
Informal description
For any fixed element $b$ in type $\beta$, the function $f : \alpha \to \alpha \times \beta$ defined by $f(a) = (a, b)$ is injective. That is, for any $a_1, a_2 \in \alpha$, if $(a_1, b) = (a_2, b)$, then $a_1 = a_2$.
Prod.mk_right_inj theorem
{a : α} {b₁ b₂ : β} : (a, b₁) = (a, b₂) ↔ b₁ = b₂
Full source 
lemma mk_right_inj {a : α} {b₁ b₂ : β} : (a, b₁)(a, b₁) = (a, b₂) ↔ b₁ = b₂ :=
    (mk_right_injective _).eq_iff
Equality of Pairs with Fixed First Component: $(a, b_1) = (a, b_2) \leftrightarrow b_1 = b_2$
Informal description
For any fixed element $a \in \alpha$ and any elements $b_1, b_2 \in \beta$, the pairs $(a, b_1)$ and $(a, b_2)$ are equal if and only if $b_1 = b_2$.
Prod.mk_left_inj theorem
{a₁ a₂ : α} {b : β} : (a₁, b) = (a₂, b) ↔ a₁ = a₂
Full source 
lemma mk_left_inj {a₁ a₂ : α} {b : β} : (a₁, b)(a₁, b) = (a₂, b) ↔ a₁ = a₂ := (mk_left_injective _).eq_iff
Equality of Pairs with Fixed Second Component: $(a_1, b) = (a_2, b) \leftrightarrow a_1 = a_2$
Informal description
For any elements $a_1, a_2 \in \alpha$ and any fixed element $b \in \beta$, the pairs $(a_1, b)$ and $(a_2, b)$ are equal if and only if $a_1 = a_2$.
Prod.map_def theorem
{f : α → γ} {g : β → δ} : Prod.map f g = fun p : α × β ↦ (f p.1, g p.2)
Full source 
theorem map_def {f : α → γ} {g : β → δ} : Prod.map f g = fun p : α × β ↦ (f p.1, g p.2) :=
  funext fun p ↦ Prod.ext (map_fst f g p) (map_snd f g p)
Definition of Product Map: $\text{Prod.map}\,f\,g = \lambda (a, b), (f(a), g(b))$
Informal description
For any functions $f : \alpha \to \gamma$ and $g : \beta \to \delta$, the product map $\text{Prod.map}\,f\,g$ is equal to the function that maps a pair $(a, b) \in \alpha \times \beta$ to $(f(a), g(b))$.
Prod.id_prod theorem
: (fun p : α × β ↦ (p.1, p.2)) = id
Full source 
theorem id_prod : (fun p : α × β ↦ (p.1, p.2)) = id :=
  rfl
Identity Function on Product Type
Informal description
The function that maps a pair $(x, y)$ to itself (i.e., the identity function on the product type $\alpha \times \beta$) is equal to the identity function $\text{id}$.
Prod.map_iterate theorem
(f : α → α) (g : β → β) (n : ℕ) : (Prod.map f g)^[n] = Prod.map f^[n] g^[n]
Full source 
@[simp]
theorem map_iterate (f : α → α) (g : β → β) (n : ℕ) :
    (Prod.map f g)^[n] = Prod.map f^[n] g^[n] := by induction n <;> simp [*, Prod.map_comp_map]
Iteration of Product Map Equals Product of Iterations
Informal description
For any functions $f : \alpha \to \alpha$ and $g : \beta \to \beta$, and any natural number $n$, the $n$-th iterate of the product map $\text{Prod.map}\,f\,g$ is equal to the product map of the $n$-th iterates of $f$ and $g$. That is, $(f \times g)^n = f^n \times g^n$.
Prod.fst_surjective theorem
[h : Nonempty β] : Function.Surjective (@fst α β)
Full source 
theorem fst_surjective [h : Nonempty β] : Function.Surjective (@fst α β) :=
  fun x ↦ h.elim fun y ↦ ⟨⟨x, y⟩, rfl⟩
Surjectivity of the First Projection on Nonempty Product Types
Informal description
For any nonempty type $\beta$, the first projection function $\operatorname{fst} : \alpha \times \beta \to \alpha$ is surjective. That is, for every $a \in \alpha$, there exists a pair $(a, b) \in \alpha \times \beta$ such that $\operatorname{fst}(a, b) = a$.
Prod.snd_surjective theorem
[h : Nonempty α] : Function.Surjective (@snd α β)
Full source 
theorem snd_surjective [h : Nonempty α] : Function.Surjective (@snd α β) :=
  fun y ↦ h.elim fun x ↦ ⟨⟨x, y⟩, rfl⟩
Surjectivity of the Second Projection on Nonempty Product Types
Informal description
For any nonempty type $\alpha$, the second projection function $\operatorname{snd} : \alpha \times \beta \to \beta$ is surjective. That is, for every $b \in \beta$, there exists a pair $(a, b) \in \alpha \times \beta$ such that $\operatorname{snd}(a, b) = b$.
Prod.fst_injective theorem
[Subsingleton β] : Function.Injective (@fst α β)
Full source 
theorem fst_injective [Subsingleton β] : Function.Injective (@fst α β) :=
  fun _ _ h ↦ Prod.ext h (Subsingleton.elim _ _)
Injectivity of First Projection on Product with Subsingleton Type
Informal description
For any type $\beta$ that is a subsingleton (i.e., all elements of $\beta$ are equal), the first projection function $\operatorname{fst} : \alpha \times \beta \to \alpha$ is injective. That is, for any pairs $(a_1, b_1), (a_2, b_2) \in \alpha \times \beta$, if $\operatorname{fst}(a_1, b_1) = \operatorname{fst}(a_2, b_2)$, then $(a_1, b_1) = (a_2, b_2)$.
Prod.snd_injective theorem
[Subsingleton α] : Function.Injective (@snd α β)
Full source 
theorem snd_injective [Subsingleton α] : Function.Injective (@snd α β) :=
  fun _ _ h ↦ Prod.ext (Subsingleton.elim _ _) h
Injectivity of Second Projection on Product Type with Subsingleton First Component
Informal description
For any types $\alpha$ and $\beta$, if $\alpha$ is a subsingleton (i.e., all elements of $\alpha$ are equal), then the second projection function $\operatorname{snd} : \alpha \times \beta \to \beta$ is injective.
Prod.swap_leftInverse theorem
: Function.LeftInverse (@swap α β) swap
Full source 
@[simp]
theorem swap_leftInverse : Function.LeftInverse (@swap α β) swap :=
  swap_swap
Swap is its own left inverse
Informal description
The function $\text{swap} : \alpha \times \beta \to \beta \times \alpha$ is a left inverse of itself, meaning that for any pair $(x, y) \in \alpha \times \beta$, we have $\text{swap}(\text{swap}(x, y)) = (x, y)$.
Prod.swap_rightInverse theorem
: Function.RightInverse (@swap α β) swap
Full source 
@[simp]
theorem swap_rightInverse : Function.RightInverse (@swap α β) swap :=
  swap_swap
Swap is its own right inverse
Informal description
The swap function on pairs, which maps $(x, y) \in \alpha \times \beta$ to $(y, x) \in \beta \times \alpha$, is a right inverse of itself. That is, for any pair $(y, x) \in \beta \times \alpha$, we have $\text{swap}(\text{swap}(y, x)) = (y, x)$.
Prod.swap_injective theorem
: Function.Injective (@swap α β)
Full source 
theorem swap_injective : Function.Injective (@swap α β) :=
  swap_leftInverse.injective
Injectivity of the Pair Swap Function
Informal description
The swap function on pairs, which maps $(x, y) \in \alpha \times \beta$ to $(y, x) \in \beta \times \alpha$, is injective. That is, for any pairs $(x_1, y_1), (x_2, y_2) \in \alpha \times \beta$, if $\text{swap}(x_1, y_1) = \text{swap}(x_2, y_2)$, then $(x_1, y_1) = (x_2, y_2)$.
Prod.swap_surjective theorem
: Function.Surjective (@swap α β)
Full source 
theorem swap_surjective : Function.Surjective (@swap α β) :=
  swap_leftInverse.surjective
Surjectivity of the Pair Swap Function
Informal description
The swap function on pairs, which maps $(x, y) \in \alpha \times \beta$ to $(y, x) \in \beta \times \alpha$, is surjective. That is, for any pair $(b, a) \in \beta \times \alpha$, there exists a pair $(a, b) \in \alpha \times \beta$ such that $\text{swap}(a, b) = (b, a)$.
Prod.swap_bijective theorem
: Function.Bijective (@swap α β)
Full source 
theorem swap_bijective : Function.Bijective (@swap α β) :=
  ⟨swap_injective, swap_surjective⟩
Bijectivity of the Pair Swap Function
Informal description
The swap function on pairs, which maps $(x, y) \in \alpha \times \beta$ to $(y, x) \in \beta \times \alpha$, is bijective. That is, it is both injective (distinct pairs map to distinct swapped pairs) and surjective (every pair in $\beta \times \alpha$ is the image of some pair in $\alpha \times \beta$ under the swap operation).
Function.Semiconj.swap_map theorem
(f : α → α) (g : β → β) : Function.Semiconj swap (map f g) (map g f)
Full source 
theorem _root_.Function.Semiconj.swap_map (f : α → α) (g : β → β) :
    Function.Semiconj swap (map f g) (map g f) :=
  Function.semiconj_iff_comp_eq.2 (map_comp_swap g f).symm
Semiconjugacy of Swap with Component-wise Maps
Informal description
For any functions $f : \alpha \to \alpha$ and $g : \beta \to \beta$, the swap function on $\alpha \times \beta$ semiconjugates the map $(f, g)$ to the map $(g, f)$. That is, for any pair $(x, y) \in \alpha \times \beta$, we have $\text{swap}(f(x), g(y)) = (g, f)(\text{swap}(x, y))$.
Prod.fst_eq_iff theorem
: ∀ {p : α × β} {x : α}, p.1 = x ↔ p = (x, p.2)
Full source 
theorem fst_eq_iff : ∀ {p : α × β} {x : α}, p.1 = x ↔ p = (x, p.2)
  | ⟨a, b⟩, x => by simp
Equality of First Component in Product Pair
Informal description
For any pair $p = (a, b)$ in the product type $\alpha \times \beta$ and any element $x \in \alpha$, the first component of $p$ equals $x$ if and only if $p$ is equal to the pair $(x, b)$.
Prod.snd_eq_iff theorem
: ∀ {p : α × β} {x : β}, p.2 = x ↔ p = (p.1, x)
Full source 
theorem snd_eq_iff : ∀ {p : α × β} {x : β}, p.2 = x ↔ p = (p.1, x)
  | ⟨a, b⟩, x => by simp
Equivalence of Second Component Equality and Pair Reconstruction
Informal description
For any pair $p = (a, b)$ in the product type $\alpha \times \beta$ and any element $x \in \beta$, the second component of $p$ equals $x$ if and only if $p$ is equal to the pair $(a, x)$.
Prod.lex_iff theorem
: Prod.Lex r s x y ↔ r x.1 y.1 ∨ x.1 = y.1 ∧ s x.2 y.2
Full source 
lemma lex_iff : Prod.LexProd.Lex r s x y ↔ r x.1 y.1 ∨ x.1 = y.1 ∧ s x.2 y.2 := lex_def
Characterization of Lexicographic Order on Product Types
Informal description
For any relations $r$ on $\alpha$ and $s$ on $\beta$, and any pairs $x, y \in \alpha \times \beta$, the lexicographic order $x <_{lex} y$ holds if and only if either the first component of $x$ is related to the first component of $y$ via $r$, or the first components are equal and the second component of $x$ is related to the second component of $y$ via $s$. In symbols: $$x <_{lex} y \iff r(x_1, y_1) \lor (x_1 = y_1 \land s(x_2, y_2))$$
Prod.Lex.decidable instance
[DecidableEq α] (r : α → α → Prop) (s : β → β → Prop) [DecidableRel r] [DecidableRel s] : DecidableRel (Prod.Lex r s)
Full source 
instance Lex.decidable [DecidableEq α]
    (r : α → α → Prop) (s : β → β → Prop) [DecidableRel r] [DecidableRel s] :
    DecidableRel (Prod.Lex r s) :=
  fun _ _ ↦ decidable_of_decidable_of_iff lex_def.symm
Decidability of Lexicographic Order on Product Types
Informal description
For types $\alpha$ and $\beta$ with decidable equality on $\alpha$ and decidable relations $r$ on $\alpha$ and $s$ on $\beta$, the lexicographic order relation $\text{Prod.Lex}\ r\ s$ on the product type $\alpha \times \beta$ is decidable.
Prod.Lex.refl_left theorem
(r : α → α → Prop) (s : β → β → Prop) [IsRefl α r] : ∀ x, Prod.Lex r s x x
Full source 
@[refl]
theorem Lex.refl_left (r : α → α → Prop) (s : β → β → Prop) [IsRefl α r] : ∀ x, Prod.Lex r s x x
  | (_, _) => Lex.left _ _ (refl _)
Reflexivity of Lexicographic Order (Left Component)
Informal description
For any reflexive relation $r$ on a type $\alpha$ and any relation $s$ on a type $\beta$, the lexicographic order $\text{Prod.Lex}\,r\,s$ on $\alpha \times \beta$ is reflexive. That is, for every $x \in \alpha \times \beta$, we have $\text{Prod.Lex}\,r\,s\,x\,x$.
Prod.instIsReflLex instance
{r : α → α → Prop} {s : β → β → Prop} [IsRefl α r] : IsRefl (α × β) (Prod.Lex r s)
Full source 
instance {r : α → α → Prop} {s : β → β → Prop} [IsRefl α r] : IsRefl (α × β) (Prod.Lex r s) :=
  ⟨Lex.refl_left _ _⟩
Reflexivity of Lexicographic Order on Product Types
Informal description
For any reflexive relation $r$ on a type $\alpha$ and any relation $s$ on a type $\beta$, the lexicographic order $\mathrm{Lex}(r,s)$ on the product type $\alpha \times \beta$ is reflexive.
Prod.Lex.refl_right theorem
(r : α → α → Prop) (s : β → β → Prop) [IsRefl β s] : ∀ x, Prod.Lex r s x x
Full source 
@[refl]
theorem Lex.refl_right (r : α → α → Prop) (s : β → β → Prop) [IsRefl β s] : ∀ x, Prod.Lex r s x x
  | (_, _) => Lex.right _ (refl _)
Reflexivity of Lexicographic Order Under Reflexive Right Relation
Informal description
For any reflexive relations $r$ on $\alpha$ and $s$ on $\beta$, if $s$ is reflexive (i.e., $\forall y \in \beta, s(y,y)$ holds), then the lexicographic order $\mathrm{Lex}(r,s)$ on $\alpha \times \beta$ is reflexive (i.e., $\forall x \in \alpha \times \beta, \mathrm{Lex}(r,s)(x,x)$ holds).
Prod.instIsReflLex_1 instance
{r : α → α → Prop} {s : β → β → Prop} [IsRefl β s] : IsRefl (α × β) (Prod.Lex r s)
Full source 
instance {r : α → α → Prop} {s : β → β → Prop} [IsRefl β s] : IsRefl (α × β) (Prod.Lex r s) :=
  ⟨Lex.refl_right _ _⟩
Reflexivity of Lexicographic Order with Reflexive Right Relation
Informal description
For any reflexive relation $s$ on $\beta$, the lexicographic order $\mathrm{Lex}(r,s)$ on $\alpha \times \beta$ is reflexive for any relation $r$ on $\alpha$.
Prod.Lex.trans theorem
{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
Full source 
@[trans]
theorem Lex.trans {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
  | (_, _), (_, _), (_, _), left  _ _ hxy₁, left  _ _ hyz₁ => left  _ _ (_root_.trans hxy₁ hyz₁)
  | (_, _), (_, _), (_, _), left  _ _ hxy₁, right _ _      => left  _ _ hxy₁
  | (_, _), (_, _), (_, _), right _ _,      left  _ _ hyz₁ => left  _ _ hyz₁
  | (_, _), (_, _), (_, _), right _ hxy₂,   right _ hyz₂   => right _ (_root_.trans hxy₂ hyz₂)
Transitivity of Lexicographic Order on Product Types
Informal description
Let $r$ be a transitive relation on a type $\alpha$ and $s$ be a transitive relation on a type $\beta$. For any three elements $x, y, z$ in the product type $\alpha \times \beta$, if $x$ is lexicographically less than $y$ with respect to $r$ and $s$, and $y$ is lexicographically less than $z$ with respect to $r$ and $s$, then $x$ is lexicographically less than $z$ with respect to $r$ and $s$.
Prod.instIsTransLex instance
{r : α → α → Prop} {s : β → β → Prop} [IsTrans α r] [IsTrans β s] : IsTrans (α × β) (Prod.Lex r s)
Full source 
instance {r : α → α → Prop} {s : β → β → Prop} [IsTrans α r] [IsTrans β s] :
  IsTrans (α × β) (Prod.Lex r s) :=
  ⟨fun _ _ _ ↦ Lex.trans⟩
Transitivity of Lexicographic Order on Products
Informal description
For any transitive relations $r$ on $\alpha$ and $s$ on $\beta$, the lexicographic order $\mathrm{Lex}(r, s)$ on $\alpha \times \beta$ is transitive.
Prod.instIsAntisymmLexOfIsStrictOrder instance
{r : α → α → Prop} {s : β → β → Prop} [IsStrictOrder α r] [IsAntisymm β s] : IsAntisymm (α × β) (Prod.Lex r s)
Full source 
instance {r : α → α → Prop} {s : β → β → Prop} [IsStrictOrder α r] [IsAntisymm β s] :
    IsAntisymm (α × β) (Prod.Lex r s) :=
  ⟨fun x₁ x₂ h₁₂ h₂₁ ↦
    match x₁, x₂, h₁₂, h₂₁ with
    | (a, _), (_, _), .left  _ _ hr₁, .left  _ _ hr₂ => (irrefl a (_root_.trans hr₁ hr₂)).elim
    | (_, _), (_, _), .left  _ _ hr₁, .right _ _     => (irrefl _ hr₁).elim
    | (_, _), (_, _), .right _ _,     .left  _ _ hr₂ => (irrefl _ hr₂).elim
    | (_, _), (_, _), .right _ hs₁,   .right _ hs₂   => antisymm hs₁ hs₂ ▸ rfl⟩
Antisymmetry of Lexicographic Order from Strict Order and Antisymmetric Relation
Informal description
For any strict order $r$ on $\alpha$ and any antisymmetric relation $s$ on $\beta$, the lexicographic order $\mathrm{Lex}(r, s)$ on $\alpha \times \beta$ is antisymmetric.
Prod.isTotal_left instance
{r : α → α → Prop} {s : β → β → Prop} [IsTotal α r] : IsTotal (α × β) (Prod.Lex r s)
Full source 
instance isTotal_left {r : α → α → Prop} {s : β → β → Prop} [IsTotal α r] :
    IsTotal (α × β) (Prod.Lex r s) :=
  ⟨fun ⟨a₁, _⟩ ⟨a₂, _⟩ ↦ (IsTotal.total a₁ a₂).imp (Lex.left _ _) (Lex.left _ _)⟩
Lexicographic Order is Total When First Component is Total
Informal description
For any relations $r$ on $\alpha$ and $s$ on $\beta$, if $r$ is a total order on $\alpha$, then the lexicographic order $\mathrm{Lex}(r, s)$ is a total order on the product $\alpha \times \beta$.
Prod.isTotal_right instance
{r : α → α → Prop} {s : β → β → Prop} [IsTrichotomous α r] [IsTotal β s] : IsTotal (α × β) (Prod.Lex r s)
Full source 
instance isTotal_right {r : α → α → Prop} {s : β → β → Prop} [IsTrichotomous α r] [IsTotal β s] :
    IsTotal (α × β) (Prod.Lex r s) :=
  ⟨fun ⟨i, a⟩ ⟨j, b⟩ ↦ by
    obtain hij | rfl | hji := trichotomous_of r i j
    · exact Or.inl (.left _ _ hij)
    · exact (total_of s a b).imp (.right _) (.right _)
    · exact Or.inr (.left _ _ hji) ⟩
Totality of Lexicographic Order with Trichotomous and Total Relations
Informal description
For any relations $r$ on $\alpha$ and $s$ on $\beta$, if $r$ is trichotomous and $s$ is total, then the lexicographic order on $\alpha \times \beta$ is total.
Prod.IsTrichotomous instance
[IsTrichotomous α r] [IsTrichotomous β s] : IsTrichotomous (α × β) (Prod.Lex r s)
Full source 
instance IsTrichotomous [IsTrichotomous α r] [IsTrichotomous β s] :
  IsTrichotomous (α × β) (Prod.Lex r s) :=
⟨fun ⟨i, a⟩ ⟨j, b⟩ ↦ by
  obtain hij | rfl | hji := trichotomous_of r i j
  { exact Or.inl (Lex.left _ _ hij) }
  { exact (trichotomous_of (s) a b).imp3 (Lex.right _) (congr_arg _) (Lex.right _) }
  { exact Or.inr (Or.inr <| Lex.left _ _ hji) }⟩
Trichotomy of Lexicographic Order from Trichotomous Relations
Informal description
For any relations $r$ on $\alpha$ and $s$ on $\beta$, if both $r$ and $s$ are trichotomous, then the lexicographic order on $\alpha \times \beta$ is also trichotomous.
Prod.instIsAsymmLex instance
[IsAsymm α r] [IsAsymm β s] : IsAsymm (α × β) (Prod.Lex r s)
Full source 
instance [IsAsymm α r] [IsAsymm β s] :
    IsAsymm (α × β) (Prod.Lex r s) where
  asymm
  | (_a₁, _a₂), (_b₁, _b₂), .left _ _ h₁, .left _ _ h₂ => IsAsymm.asymm _ _ h₂ h₁
  | (_a₁, _a₂), (_, _b₂), .left _ _ h₁, .right _ _ => IsAsymm.asymm _ _ h₁ h₁
  | (_a₁, _a₂), (_, _b₂), .right _ _, .left _ _ h₂ => IsAsymm.asymm _ _ h₂ h₂
  | (_a₁, _a₂), (_, _b₂), .right _ h₁, .right _ h₂ => IsAsymm.asymm _ _ h₁ h₂
Asymmetry of Lexicographic Order from Asymmetric Relations
Informal description
For any relations $r$ on $\alpha$ and $s$ on $\beta$, if both $r$ and $s$ are asymmetric, then the lexicographic order on $\alpha \times \beta$ is also asymmetric.
Function.Injective.prodMap theorem
(hf : Injective f) (hg : Injective g) : Injective (map f g)
Full source 
theorem Injective.prodMap (hf : Injective f) (hg : Injective g) : Injective (map f g) :=
  fun _ _ h ↦ Prod.ext (hf <| congr_arg Prod.fst h) (hg <| congr_arg Prod.snd h)
Injectivity of Product Map from Component Injections
Informal description
Given two injective functions $f : \alpha \to \gamma$ and $g : \beta \to \delta$, the product map $(f \times g) : \alpha \times \beta \to \gamma \times \delta$ defined by $(f \times g)(a, b) = (f(a), g(b))$ is also injective.
Function.Surjective.prodMap theorem
(hf : Surjective f) (hg : Surjective g) : Surjective (map f g)
Full source 
theorem Surjective.prodMap (hf : Surjective f) (hg : Surjective g) : Surjective (map f g) :=
  fun p ↦
  let ⟨x, hx⟩ := hf p.1
  let ⟨y, hy⟩ := hg p.2
  ⟨(x, y), Prod.ext hx hy⟩
Surjectivity of Product Map
Informal description
If $f : \alpha \to \beta$ and $g : \gamma \to \delta$ are surjective functions, then their product map $f \times g : \alpha \times \gamma \to \beta \times \delta$ is also surjective.
Function.Bijective.prodMap theorem
(hf : Bijective f) (hg : Bijective g) : Bijective (map f g)
Full source 
theorem Bijective.prodMap (hf : Bijective f) (hg : Bijective g) : Bijective (map f g) :=
  ⟨hf.1.prodMap hg.1, hf.2.prodMap hg.2⟩
Bijectivity of Product Map from Component Bijections
Informal description
Given two bijective functions $f : \alpha \to \gamma$ and $g : \beta \to \delta$, the product map $(f \times g) : \alpha \times \beta \to \gamma \times \delta$ defined by $(f \times g)(a, b) = (f(a), g(b))$ is also bijective.
Function.LeftInverse.prodMap theorem
(hf : LeftInverse f₁ f₂) (hg : LeftInverse g₁ g₂) : LeftInverse (map f₁ g₁) (map f₂ g₂)
Full source 
theorem LeftInverse.prodMap (hf : LeftInverse f₁ f₂) (hg : LeftInverse g₁ g₂) :
    LeftInverse (map f₁ g₁) (map f₂ g₂) :=
  fun a ↦ by rw [Prod.map_map, hf.comp_eq_id, hg.comp_eq_id, map_id, id]
Left Inverse Property of Product Maps
Informal description
Given functions $f_1 : \alpha \to \gamma$ and $f_2 : \gamma \to \alpha$ such that $f_1$ is a left inverse of $f_2$, and functions $g_1 : \beta \to \delta$ and $g_2 : \delta \to \beta$ such that $g_1$ is a left inverse of $g_2$, then the product map $(f_1 \times g_1) : \alpha \times \beta \to \gamma \times \delta$ is a left inverse of the product map $(f_2 \times g_2) : \gamma \times \delta \to \alpha \times \beta$.
Function.RightInverse.prodMap theorem
: RightInverse f₁ f₂ → RightInverse g₁ g₂ → RightInverse (map f₁ g₁) (map f₂ g₂)
Full source 
theorem RightInverse.prodMap :
    RightInverse f₁ f₂ → RightInverse g₁ g₂ → RightInverse (map f₁ g₁) (map f₂ g₂) :=
  LeftInverse.prodMap
Right Inverse Property of Product Maps
Informal description
Given functions $f_1 : \gamma \to \alpha$ and $f_2 : \alpha \to \gamma$ such that $f_1$ is a right inverse of $f_2$, and functions $g_1 : \delta \to \beta$ and $g_2 : \beta \to \delta$ such that $g_1$ is a right inverse of $g_2$, then the product map $(f_1 \times g_1) : \gamma \times \delta \to \alpha \times \beta$ is a right inverse of the product map $(f_2 \times g_2) : \alpha \times \beta \to \gamma \times \delta$.
Function.Involutive.prodMap theorem
{f : α → α} {g : β → β} : Involutive f → Involutive g → Involutive (map f g)
Full source 
theorem Involutive.prodMap {f : α → α} {g : β → β} :
    Involutive f → Involutive g → Involutive (map f g) :=
  LeftInverse.prodMap
Product of Involutive Functions is Involutive
Informal description
Let $f : \alpha \to \alpha$ and $g : \beta \to \beta$ be involutive functions. Then the product map $f \times g : \alpha \times \beta \to \alpha \times \beta$ defined by $(f \times g)(a, b) = (f(a), g(b))$ is also involutive.
Prod.map_injective theorem
[Nonempty α] [Nonempty β] {f : α → γ} {g : β → δ} : Injective (map f g) ↔ Injective f ∧ Injective g
Full source 
@[simp]
theorem map_injective [Nonempty α] [Nonempty β] {f : α → γ} {g : β → δ} :
    InjectiveInjective (map f g) ↔ Injective f ∧ Injective g :=
  ⟨fun h =>
    ⟨fun a₁ a₂ ha => by
      inhabit β
      injection
        @h (a₁, default) (a₂, default) (congr_arg (fun c : γ => Prod.mk c (g default)) ha :),
      fun b₁ b₂ hb => by
      inhabit α
      injection @h (default, b₁) (default, b₂) (congr_arg (Prod.mk (f default)) hb :)⟩,
    fun h => h.1.prodMap h.2⟩
Injectivity of Product Map Equivalence
Informal description
Let $\alpha$, $\beta$, $\gamma$, $\delta$ be nonempty types, and let $f : \alpha \to \gamma$ and $g : \beta \to \delta$ be functions. The product map $f \times g : \alpha \times \beta \to \gamma \times \delta$ defined by $(f \times g)(a, b) = (f(a), g(b))$ is injective if and only if both $f$ and $g$ are injective.
Prod.map_surjective theorem
[Nonempty γ] [Nonempty δ] {f : α → γ} {g : β → δ} : Surjective (map f g) ↔ Surjective f ∧ Surjective g
Full source 
@[simp]
theorem map_surjective [Nonempty γ] [Nonempty δ] {f : α → γ} {g : β → δ} :
    SurjectiveSurjective (map f g) ↔ Surjective f ∧ Surjective g :=
  ⟨fun h =>
    ⟨fun c => by
      inhabit δ
      obtain ⟨⟨a, b⟩, h⟩ := h (c, default)
      exact ⟨a, congr_arg Prod.fst h⟩,
      fun d => by
      inhabit γ
      obtain ⟨⟨a, b⟩, h⟩ := h (default, d)
      exact ⟨b, congr_arg Prod.snd h⟩⟩,
    fun h => h.1.prodMap h.2⟩
Surjectivity of Product Map Equivalence
Informal description
Let $\alpha$, $\beta$, $\gamma$, $\delta$ be nonempty types, and let $f : \alpha \to \gamma$ and $g : \beta \to \delta$ be functions. The product map $f \times g : \alpha \times \beta \to \gamma \times \delta$ is surjective if and only if both $f$ and $g$ are surjective.
Prod.map_bijective theorem
[Nonempty α] [Nonempty β] {f : α → γ} {g : β → δ} : Bijective (map f g) ↔ Bijective f ∧ Bijective g
Full source 
@[simp]
theorem map_bijective [Nonempty α] [Nonempty β] {f : α → γ} {g : β → δ} :
    BijectiveBijective (map f g) ↔ Bijective f ∧ Bijective g := by
  haveI := Nonempty.map f ‹_›
  haveI := Nonempty.map g ‹_›
  exact (map_injective.and map_surjective).trans and_and_and_comm
Bijectivity of Product Map Equivalence
Informal description
Let $\alpha$, $\beta$, $\gamma$, $\delta$ be nonempty types, and let $f : \alpha \to \gamma$ and $g : \beta \to \delta$ be functions. The product map $f \times g : \alpha \times \beta \to \gamma \times \delta$ defined by $(f \times g)(a, b) = (f(a), g(b))$ is bijective if and only if both $f$ and $g$ are bijective.
Prod.map_leftInverse theorem
[Nonempty β] [Nonempty δ] {f₁ : α → β} {g₁ : γ → δ} {f₂ : β → α} {g₂ : δ → γ} : LeftInverse (map f₁ g₁) (map f₂ g₂) ↔ LeftInverse f₁ f₂ ∧ LeftInverse g₁ g₂
Full source 
@[simp]
theorem map_leftInverse [Nonempty β] [Nonempty δ] {f₁ : α → β} {g₁ : γ → δ} {f₂ : β → α}
    {g₂ : δ → γ} : LeftInverseLeftInverse (map f₁ g₁) (map f₂ g₂) ↔ LeftInverse f₁ f₂ ∧ LeftInverse g₁ g₂ :=
  ⟨fun h =>
    ⟨fun b => by
      inhabit δ
      exact congr_arg Prod.fst (h (b, default)),
      fun d => by
      inhabit β
      exact congr_arg Prod.snd (h (default, d))⟩,
    fun h => h.1.prodMap h.2 ⟩
Left Inverse Property of Product Maps Equivalence
Informal description
Let $\beta$ and $\delta$ be nonempty types, and let $f_1 : \alpha \to \beta$, $g_1 : \gamma \to \delta$, $f_2 : \beta \to \alpha$, and $g_2 : \delta \to \gamma$ be functions. The product map $(f_1 \times g_1) : \alpha \times \gamma \to \beta \times \delta$ is a left inverse of the product map $(f_2 \times g_2) : \beta \times \delta \to \alpha \times \gamma$ if and only if $f_1$ is a left inverse of $f_2$ and $g_1$ is a left inverse of $g_2$. That is, for all $x \in \alpha$ and $y \in \gamma$, we have $f_1(f_2(x)) = x$ and $g_1(g_2(y)) = y$.
Prod.map_rightInverse theorem
[Nonempty α] [Nonempty γ] {f₁ : α → β} {g₁ : γ → δ} {f₂ : β → α} {g₂ : δ → γ} : RightInverse (map f₁ g₁) (map f₂ g₂) ↔ RightInverse f₁ f₂ ∧ RightInverse g₁ g₂
Full source 
@[simp]
theorem map_rightInverse [Nonempty α] [Nonempty γ] {f₁ : α → β} {g₁ : γ → δ} {f₂ : β → α}
    {g₂ : δ → γ} : RightInverseRightInverse (map f₁ g₁) (map f₂ g₂) ↔ RightInverse f₁ f₂ ∧ RightInverse g₁ g₂ :=
  map_leftInverse
Right Inverse Property of Product Maps Equivalence
Informal description
Let $\alpha$, $\gamma$, $\beta$, $\delta$ be nonempty types, and let $f_1 : \alpha \to \beta$, $g_1 : \gamma \to \delta$, $f_2 : \beta \to \alpha$, and $g_2 : \delta \to \gamma$ be functions. The product map $(f_1 \times g_1) : \alpha \times \gamma \to \beta \times \delta$ is a right inverse of the product map $(f_2 \times g_2) : \beta \times \delta \to \alpha \times \gamma$ if and only if $f_1$ is a right inverse of $f_2$ and $g_1$ is a right inverse of $g_2$. That is, for all $x \in \beta$ and $y \in \delta$, we have $f_2(f_1(x)) = x$ and $g_2(g_1(y)) = y$.
Prod.map_involutive theorem
[Nonempty α] [Nonempty β] {f : α → α} {g : β → β} : Involutive (map f g) ↔ Involutive f ∧ Involutive g
Full source 
@[simp]
theorem map_involutive [Nonempty α] [Nonempty β] {f : α → α} {g : β → β} :
    InvolutiveInvolutive (map f g) ↔ Involutive f ∧ Involutive g :=
  map_leftInverse
Involutive Property of Product Maps Equivalence
Informal description
Let $\alpha$ and $\beta$ be nonempty types, and let $f : \alpha \to \alpha$ and $g : \beta \to \beta$ be functions. The product map $(f \times g) : \alpha \times \beta \to \alpha \times \beta$ is involutive if and only if both $f$ and $g$ are involutive. That is, for all $(x, y) \in \alpha \times \beta$, we have $(f \times g)((f \times g)(x, y)) = (x, y)$ if and only if $f(f(x)) = x$ and $g(g(y)) = y$ for all $x \in \alpha$ and $y \in \beta$.
Prod.PrettyPrinting.pp.numericProj.prod opaque
: Lean.Option✝ Bool
Full source 
/--
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`.
-/
register_option pp.numericProj.prod : Bool := {
  defValue := true
  descr := "enable pretty printing `Prod.fst x` as `x.1` and `Prod.snd x` as `x.2`."
}
Numeric Projection Pretty-Printing Option for Product Types
Informal description
This option controls whether the first and second projections of a product type `Prod α β` should be pretty-printed using numeric notation (`x.1` and `x.2`) instead of the standard notation (`x.fst` and `x.snd`).
Prod.PrettyPrinting.getPPNumericProjProd definition
(o : Options) : Bool
Full source 
/-- Tell whether pretty-printing should use numeric projection notations `.1`
and `.2` for `Prod.fst` and `Prod.snd`. -/
def getPPNumericProjProd (o : Options) : Bool :=
  o.get pp.numericProj.prod.name pp.numericProj.prod.defValue
Get numeric projection pretty-printing setting for product types
Informal description
The function retrieves the current setting for whether numeric projection notation (`.1` and `.2`) should be used when pretty-printing the first and second projections of a product type `Prod α β`. The setting is stored in the options object `o` and defaults to `pp.numericProj.prod.defValue` if not explicitly set.
Prod.PrettyPrinting.delabProdFst definition
: Delab
Full source 
/-- Delaborator for `Prod.fst x` as `x.1`. -/
@[app_delab Prod.fst]
def delabProdFst : Delab :=
  whenPPOption getPPNumericProjProd <|
  whenPPOption getPPFieldNotation <|
  whenNotPPOption getPPExplicit <|
  withOverApp 3 do
    let x ← SubExpr.withAppArg delab
    `($(x).1)
First projection delaborator for product types
Informal description
The delaborator for `Prod.fst x` that formats it as `x.1` when pretty-printing, using numeric projection notation for the first component of a product type.
Prod.PrettyPrinting.delabProdSnd definition
: Delab
Full source 
/-- Delaborator for `Prod.snd x` as `x.2`. -/
@[app_delab Prod.snd]
def delabProdSnd : Delab :=
  whenPPOption getPPNumericProjProd <|
  whenPPOption getPPFieldNotation <|
  whenNotPPOption getPPExplicit <|
  withOverApp 3 do
    let x ← SubExpr.withAppArg delab
    `($(x).2)
Second projection delaborator for product types
Informal description
The delaborator for `Prod.snd x` that formats it as `x.2` when pretty-printing, using numeric projection notation for the second component of a product type.