map_snd_pair — Mathlib

English

Let f: α →ₛ β and g: α →ₛ γ be simple functions. If we form the pair (f, g) and then project onto the second component, we recover g.

Русский

Пусть f: α →ₛ β и g: α →ₛ γ — простые функции. Если образовать пару (f, g) и затем проецировать на вторую компоненту, получим g.

LaTeX

$$$((f \text{.pair } g).map \operatorname{Prod.snd}) = g$$$

Lean4

@[simp]
theorem map_snd_pair (f : α →ₛ β) (g : α →ₛ γ) : (f.pair g).map Prod.snd = g :=
  rfl

Похожие утверждения