source
instance Prod.instReflBEq {α : Type u_1} {β : Type u_2} [BEq α] [BEq β] [ReflBEq α] [ReflBEq β] :
ReflBEq (α × β)
source
instance Prod.instLawfulBEq {α : Type u_1} {β : Type u_2} [BEq α] [BEq β] [LawfulBEq α] [LawfulBEq β] :
LawfulBEq (α × β)
source
@[simp]
theorem Prod.forall {α : Type u_1} {β : Type u_2} {p : α × β → Prop} :
(∀ (x : α × β), p x) ↔ ∀ (a : α) (b : β), p (a, b)
source
@[simp]
theorem Prod.exists {α : Type u_1} {β : Type u_2} {p : α × β → Prop} :
(∃ (x : α × β), p x) ↔ ∃ (a : α), ∃ (b : β), p (a, b)
source
@[simp]
theorem Prod.map_id {α : Type u_1} {β : Type u_2} :
map id id = id
source
@[simp]
theorem Prod.map_id' {α : Type u_1} {β : Type u_2} :
(map (fun (a : α) => a) fun (b : β) => b) = fun (x : α × β) => x
source
theorem Prod.map_comp_map {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} {ε : Type u_5} {ζ : Type u_6} (f : α → β) (f' : γ → δ) (g : β → ε) (g' : δ → ζ) :
map g g' ∘ map f f' = map (g ∘ f) (g' ∘ f')

Composing a `Prod.map` with another `Prod.map` is equal to a single `Prod.map` of composed functions.

source
theorem Prod.map_map {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} {ε : Type u_5} {ζ : Type u_6} (f : α → β) (f' : γ → δ) (g : β → ε) (g' : δ → ζ) (x : α × γ) :
map g g' (map f f' x) = map (g ∘ f) (g' ∘ f') x

Composing a `Prod.map` with another `Prod.map` is equal to a single `Prod.map` of composed functions, fully applied.

source
def Prod.swap {α : Type u_1} {β : Type u_2} :
α × β → β × α

Swaps the elements in a pair.

Examples:

- `(1, 2).swap = (2, 1)`
- `("orange", -87).swap = (-87, "orange")`

Equations

- p.swap = (p.snd, p.fst)

Instances For

source
@[simp]
theorem Prod.swap_swap {α : Type u_1} {β : Type u_2} (x : α × β) :
x.swap.swap = x
source
@[simp]
theorem Prod.fst_swap {α : Type u_1} {β : Type u_2} {p : α × β} :
p.swap.fst = p.snd
source
@[simp]
theorem Prod.snd_swap {α : Type u_1} {β : Type u_2} {p : α × β} :
p.swap.snd = p.fst
source
@[simp]
theorem Prod.swap_prod_mk {α : Type u_1} {β : Type u_2} {a : α} {b : β} :
(a, b).swap = (b, a)
source
@[simp]
theorem Prod.swap_swap_eq {α : Type u_1} {β : Type u_2} :
swap ∘ swap = id
source
@[simp]
theorem Prod.swap_inj {α : Type u_1} {β : Type u_2} {p q : α × β} :
p.swap = q.swap ↔ p = q
source
theorem Prod.map_comp_swap {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} (f : α → β) (g : γ → δ) :
map f g ∘ swap = swap ∘ map g f

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`.