@[inline]

def Data.Tuple.swap {α : Type u_1} {β : Type u_2} (p : α × β) : β × α

Swap the components of a pair. $$\text{swap}(a, b) = (b, a)$$

Equations

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

@[inline]

def Data.Tuple.mapFst {α : Type u_1} {γ : Type u_2} {β : Type u_3} (f : α → γ) (p : α × β) : γ × β

Map over the first component of a pair. $$\text{mapFst}(f, (a, b)) = (f(a), b)$$

Equations

• Data.Tuple.mapFst f p = (f p.fst, p.snd)

@[inline]

def Data.Tuple.mapSnd {β : Type u_1} {γ : Type u_2} {α : Type u_3} (f : β → γ) (p : α × β) : α × γ

Map over the second component of a pair. $$\text{mapSnd}(f, (a, b)) = (a, f(b))$$

Equations

• Data.Tuple.mapSnd f p = (p.fst, f p.snd)

@[inline]

def Data.Tuple.bimap {α : Type u_1} {γ : Type u_2} {β : Type u_3} {δ : Type u_4} (f : α → γ) (g : β → δ) (p : α × β) : γ × δ

Map over both components of a pair simultaneously. $$\text{bimap}(f, g, (a, b)) = (f(a), g(b))$$

Equations

• Data.Tuple.bimap f g p = (f p.fst, g p.snd)

@[inline]

def Data.Tuple.curry {α : Type u_1} {β : Type u_2} {γ : Sort u_3} (f : α × β → γ) (a : α) (b : β) : γ

Curry a function on pairs into a two-argument function. $$\text{curry}(f)(a)(b) = f(a, b)$$

Equations

• Data.Tuple.curry f a b = f (a, b)

@[inline]

def Data.Tuple.uncurry {α : Type u_1} {β : Type u_2} {γ : Sort u_3} (f : α → β → γ) (p : α × β) : γ

Uncurry a two-argument function into a function on pairs. $$\text{uncurry}(f)(a, b) = f(a)(b)$$

Equations

• Data.Tuple.uncurry f p = f p.fst p.snd

theorem Data.Tuple.swap_swap {α : Type u_1} {β : Type u_2} (p : α × β) : swap (swap p) = p

Swapping twice is identity (involution). $$\text{swap}(\text{swap}(p)) = p$$

theorem Data.Tuple.curry_uncurry {α : Type u_1} {β : Type u_2} {γ : Sort u_3} (f : α → β → γ) : curry (uncurry f) = f

curry and uncurry form an isomorphism. $$\text{curry}(\text{uncurry}(f)) = f$$

theorem Data.Tuple.uncurry_curry {α : Type u_1} {β : Type u_2} {γ : Sort u_3} (f : α × β → γ) : uncurry (curry f) = f

uncurry and curry form an isomorphism. $$\text{uncurry}(\text{curry}(f)) = f$$

theorem Data.Tuple.bimap_id {α : Type u_1} {β : Type u_2} (p : α × β) : bimap id id p = p

bimap with identities is identity. $$\text{bimap}(\text{id}, \text{id}, p) = p$$

theorem Data.Tuple.bimap_comp {γ : Type u_1} {δ : Type u_2} {α : Type u_3} {ε : Type u_4} {ζ : Type u_5} {β : Type u_6} (f₁ : γ → δ) (f₂ : α → γ) (g₁ : ε → ζ) (g₂ : β → ε) (p : α × β) : bimap (f₁ ∘ f₂) (g₁ ∘ g₂) p = bimap f₁ g₁ (bimap f₂ g₂ p)

bimap distributes over composition. $$\text{bimap}(f_1 \circ f_2, g_1 \circ g_2, p) = \text{bimap}(f_1, g_1, \text{bimap}(f_2, g_2, p))$$

theorem Data.Tuple.mapFst_eq_bimap {α : Type u_1} {γ : Type u_2} {β : Type u_3} (f : α → γ) (p : α × β) : mapFst f p = bimap f id p

mapFst is bimap with identity on the second component. $$\text{mapFst}(f) = \text{bimap}(f, \text{id})$$

theorem Data.Tuple.mapSnd_eq_bimap {β : Type u_1} {γ : Type u_2} {α : Type u_3} (g : β → γ) (p : α × β) : mapSnd g p = bimap id g p

mapSnd is bimap with identity on the first component. $$\text{mapSnd}(g) = \text{bimap}(\text{id}, g)$$