Init.Data.Prod

Prod.instLawfulBEq instance

[BEq α] [BEq β] [LawfulBEq α] [LawfulBEq β] : LawfulBEq (α × β)

Full source

instance [BEq α] [BEq β] [LawfulBEq α] [LawfulBEq β] : LawfulBEq (α × β) where
  eq_of_beq {a b} (h : a.1 == b.1 && a.2 == b.2) := by
    cases a; cases b
    refine congr (congrArg _ (eq_of_beq ?_)) (eq_of_beq ?_) <;> simp_all
  rfl {a} := by cases a; simp [BEq.beq, LawfulBEq.rfl]

Lawful Boolean Equality on Product Types

Informal description

For any types $\alpha$ and $\beta$ equipped with boolean equality relations that coincide with propositional equality (i.e., `LawfulBEq` instances), the product type $\alpha \times \beta$ also has a boolean equality relation that coincides with propositional equality. Specifically, the boolean equality on pairs is defined component-wise and satisfies: 1. If $(a_1, b_1) == (a_2, b_2)$ evaluates to `true`, then $(a_1, b_1) = (a_2, b_2)$ holds. 2. For any pair $(a, b) \in \alpha \times \beta$, the test $(a, b) == (a, b)$ evaluates to `true`.

Prod.forall theorem

{p : α × β → Prop} : (∀ x, p x) ↔ ∀ a b, p (a, b)

Full source

@[simp]
protected theorem «forall» {p : α × β → Prop} : (∀ x, p x) ↔ ∀ a b, p (a, b) :=
  ⟨fun h a b ↦ h (a, b), fun h ⟨a, b⟩ ↦ h a b⟩

Universal Quantification over Product Type Components

Informal description

For any predicate $p$ on the product type $\alpha \times \beta$, the universal quantification over all pairs $(x, y) \in \alpha \times \beta$ is equivalent to the universal quantification over each component separately. That is, $(\forall x \in \alpha \times \beta, p(x)) \leftrightarrow (\forall a \in \alpha, \forall b \in \beta, p(a, b))$.

Prod.exists theorem

{p : α × β → Prop} : (∃ x, p x) ↔ ∃ a b, p (a, b)

Full source

@[simp]
protected theorem «exists» {p : α × β → Prop} : (∃ x, p x) ↔ ∃ a b, p (a, b) :=
  ⟨fun ⟨⟨a, b⟩, h⟩ ↦ ⟨a, b, h⟩, fun ⟨a, b, h⟩ ↦ ⟨⟨a, b⟩, h⟩⟩

Existential Quantification over Product Components

Informal description

For any predicate $p$ on the product type $\alpha \times \beta$, the existential quantification over pairs $(x, y) \in \alpha \times \beta$ is equivalent to the existential quantification over each component separately. That is, $(\exists x \in \alpha \times \beta, p(x)) \leftrightarrow (\exists a \in \alpha, \exists b \in \beta, p(a, b))$.

Prod.map_id theorem

: Prod.map (@id α) (@id β) = id

Full source

@[simp] theorem map_id : Prod.map (@id α) (@id β) = id := rfl

Identity Mapping Preserved Under Product Map

Informal description

For any types $\alpha$ and $\beta$, the component-wise mapping of the identity functions on $\alpha$ and $\beta$ via $\text{Prod.map}$ is equal to the identity function on the product type $\alpha \times \beta$. In other words, $\text{Prod.map}(\text{id}_\alpha, \text{id}_\beta) = \text{id}_{\alpha \times \beta}$.

Prod.map_id' theorem

: Prod.map (fun a : α => a) (fun b : β => b) = fun x ↦ x

Full source

@[simp] theorem map_id' : Prod.map (fun a : α => a) (fun b : β => b) = fun x ↦ x := rfl

Product Map of Identity Functions is Identity

Informal description

For any types $\alpha$ and $\beta$, the component-wise mapping of the identity functions (i.e., $\lambda a \mapsto a$ on $\alpha$ and $\lambda b \mapsto b$ on $\beta$) via the product map operation is equal to the identity function on $\alpha \times \beta$. In other words, $\text{Prod.map}(\text{id}_\alpha, \text{id}_\beta) = \text{id}_{\alpha \times \beta}$.

Prod.map_comp_map theorem

 (f : α → β) (f' : γ → δ) (g : β → ε) (g' : δ → ζ) : Prod.map g g' ∘ Prod.map f f' = Prod.map (g ∘ f) (g' ∘ f')

Full source

/--
Composing a `Prod.map` with another `Prod.map` is equal to
a single `Prod.map` of composed functions.
-/
theorem map_comp_map (f : α → β) (f' : γ → δ) (g : β → ε) (g' : δ → ζ) :
    Prod.mapProd.map g g' ∘ Prod.map f f' = Prod.map (g ∘ f) (g' ∘ f') :=
  rfl

Composition of Product Maps Equals Product Map of Compositions

Informal description

For any functions $f : \alpha \to \beta$, $f' : \gamma \to \delta$, $g : \beta \to \varepsilon$, and $g' : \delta \to \zeta$, the composition of the product maps satisfies: \[ \text{Prod.map}(g, g') \circ \text{Prod.map}(f, f') = \text{Prod.map}(g \circ f, g' \circ f') \]

Prod.map_map theorem

 (f : α → β) (f' : γ → δ) (g : β → ε) (g' : δ → ζ) (x : α × γ) :
  Prod.map g g' (Prod.map f f' x) = Prod.map (g ∘ f) (g' ∘ f') x

Full source

/--
Composing a `Prod.map` with another `Prod.map` is equal to
a single `Prod.map` of composed functions, fully applied.
-/
theorem map_map (f : α → β) (f' : γ → δ) (g : β → ε) (g' : δ → ζ) (x : α × γ) :
    Prod.map g g' (Prod.map f f' x) = Prod.map (g ∘ f) (g' ∘ f') x :=
  rfl

Composition of Product Maps Equals Product Map of Compositions

Informal description

For any functions $f \colon \alpha \to \beta$, $f' \colon \gamma \to \delta$, $g \colon \beta \to \varepsilon$, and $g' \colon \delta \to \zeta$, and for any ordered pair $x = (a, c) \in \alpha \times \gamma$, the following equality holds: \[ \text{Prod.map}(g, g') \big(\text{Prod.map}(f, f')(x)\big) = \text{Prod.map}(g \circ f, g' \circ f')(x). \]

Prod.swap definition

: α × β → β × α

Full source

/--
Swaps the elements in a pair.

Examples:
 * `(1, 2).swap = (2, 1)`
 * `("orange", -87).swap = (-87, "orange")`
-/
def swap : α × β → β × α := fun p => (p.2, p.1)

Swap components of an ordered pair

Informal description

The function takes an ordered pair $(a, b)$ of type $\alpha \times \beta$ and returns the pair $(b, a)$ with the components swapped.

Prod.swap_swap theorem

: ∀ x : α × β, swap (swap x) = x

Full source

@[simp]
theorem swap_swap : ∀ x : α × β, swap (swap x) = x
  | ⟨_, _⟩ => rfl

Double Swap Returns Original Pair

Informal description

For any ordered pair $x = (a, b)$ in $\alpha \times \beta$, swapping the components twice returns the original pair, i.e., $\mathrm{swap}(\mathrm{swap}(x)) = x$.

Prod.fst_swap theorem

{p : α × β} : (swap p).1 = p.2

Full source

@[simp]
theorem fst_swap {p : α × β} : (swap p).1 = p.2 :=
  rfl

First component of swapped pair equals second component

Informal description

For any ordered pair $p = (a, b)$ in $\alpha \times \beta$, the first component of the swapped pair $\mathrm{swap}(p)$ is equal to the second component of $p$, i.e., $(\mathrm{swap}(p)).1 = p.2$.

Prod.snd_swap theorem

{p : α × β} : (swap p).2 = p.1

Full source

@[simp]
theorem snd_swap {p : α × β} : (swap p).2 = p.1 :=
  rfl

Second Component of Swapped Pair Equals First Component

Informal description

For any ordered pair $p = (a, b)$ in $\alpha \times \beta$, the second component of the swapped pair $\mathrm{swap}(p)$ is equal to the first component of $p$, i.e., $(\mathrm{swap}(p)).2 = a$.

Prod.swap_prod_mk theorem

{a : α} {b : β} : swap (a, b) = (b, a)

Full source

@[simp]
theorem swap_prod_mk {a : α} {b : β} : swap (a, b) = (b, a) :=
  rfl

Swap of Ordered Pair Components: $\mathrm{swap}(a, b) = (b, a)$

Informal description

For any elements $a \in \alpha$ and $b \in \beta$, swapping the components of the ordered pair $(a, b)$ yields the pair $(b, a)$.

Prod.swap_swap_eq theorem

: swap ∘ swap = @id (α × β)

Full source

@[simp]
theorem swap_swap_eq : swapswap ∘ swap = @id (α × β) :=
  funext swap_swap

Double Swap Equals Identity: $\mathrm{swap} \circ \mathrm{swap} = \mathrm{id}$

Informal description

The composition of the swap function with itself is equal to the identity function on the product type $\alpha \times \beta$, i.e., $\mathrm{swap} \circ \mathrm{swap} = \mathrm{id}$.

Prod.swap_inj theorem

{p q : α × β} : swap p = swap q ↔ p = q

Full source

@[simp]
theorem swap_inj {p q : α × β} : swapswap p = swap q ↔ p = q := by
  cases p; cases q; simp [and_comm]

Injectivity of Swap Function on Ordered Pairs: $\mathrm{swap}(p) = \mathrm{swap}(q) \leftrightarrow p = q$

Informal description

For any ordered pairs $p, q \in \alpha \times \beta$, the equality $\mathrm{swap}(p) = \mathrm{swap}(q)$ holds if and only if $p = q$.

Prod.map_comp_swap theorem

(f : α → β) (g : γ → δ) : Prod.map f g ∘ Prod.swap = Prod.swap ∘ Prod.map g f

Full source

/--
For two functions `f` and `g`, the composition of `Prod.map f g` with `Prod.swap`
is equal to the composition of `Prod.swap` with `Prod.map g f`.
-/
theorem map_comp_swap (f : α → β) (g : γ → δ) :
    Prod.mapProd.map f g ∘ Prod.swap = Prod.swapProd.swap ∘ Prod.map g f := rfl

Commutativity of Product Map and Swap

Informal description

For any functions $f \colon \alpha \to \beta$ and $g \colon \gamma \to \delta$, the composition of $\text{Prod.map}\, f\, g$ with $\text{Prod.swap}$ is equal to the composition of $\text{Prod.swap}$ with $\text{Prod.map}\, g\, f$. In other words, the following diagram commutes: \[ \text{Prod.map}\, f\, g \circ \text{Prod.swap} = \text{Prod.swap} \circ \text{Prod.map}\, g\, f. \]