map_fst_pair — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

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

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