coe_fst — Mathlib

English

The linear map fst corresponds to the first projection function; i.e., its underlying function is the first coordinate projection.

Русский

Линейное отображение fst соответствует функции проекции на первую координату; базовое отображение равно первой координате.

LaTeX

$$$\text{coe}_{fst}: \bigl( fst\, R\, M\, M_2\bigr) = \mathrm{Prod}.fst$.$$

Lean4

@[simp, norm_cast]
theorem coe_fst : ⇑(fst R M M₂) = Prod.fst :=
  rfl

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