instance Prod.instLawfulBEq {α : Type u_1} {β : Type u_2} [BEq α] [BEq β] [LawfulBEq α] [LawfulBEq β] : LawfulBEq (α × β)

Equations

• ⋯ = ⋯

@[simp]

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

@[simp]

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

@[simp]

theorem Prod.map_id {α : Type u_1} {β : Type u_2} : Prod.map id id = id

@[simp]

theorem Prod.map_id' {α : Type u_1} {β : Type u_2} : (Prod.map (fun (a : α) => a) fun (b : β) => b) = fun (x : α × β) => x

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' : δ → ζ) : Prod.map g g' ∘ Prod.map f f' = Prod.map (g ∘ f) (g' ∘ f')

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

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 : α × γ) : Prod.map g g' (Prod.map f f' x) = Prod.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.

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

Swap the factors of a product. swap (a, b) = (b, a)

Equations

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

@[simp]

theorem Prod.swap_swap {α : Type u_1} {β : Type u_2} (x : α × β) : x.swap.swap = x

@[simp]

theorem Prod.fst_swap {α : Type u_1} {β : Type u_2} {p : α × β} : p.swap.fst = p.snd

@[simp]

theorem Prod.snd_swap {α : Type u_1} {β : Type u_2} {p : α × β} : p.swap.snd = p.fst

@[simp]

theorem Prod.swap_prod_mk {α : Type u_1} {β : Type u_2} {a : α} {b : β} : (a, b).swap = (b, a)

@[simp]

theorem Prod.swap_swap_eq {α : Type u_1} {β : Type u_2} : Prod.swap ∘ Prod.swap = id

@[simp]

theorem Prod.swap_inj {α : Type u_1} {β : Type u_2} {p : α × β} {q : α × β} : p.swap = q.swap ↔ p = q

theorem Prod.map_comp_swap {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} (f : α → β) (g : γ → δ) : Prod.map f g ∘ Prod.swap = Prod.swap ∘ Prod.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.