coe_fst'

Mathlib.Topology.Algebra.Module.LinearMapPiProd

URI: https://scilib.ai/kg/mathlib#ContinuousLinearMap.coe_fst'

English

The function part of fst is the standard first projection map on the product, i.e., it equals Prod.fst.

Русский

Функциональная часть fst равна стандартной проекции на первую координату, то есть Prod.fst.

LaTeX

$$$\uparrow(\mathrm{fst}\ R\ M_1\ M_2) = \mathrm{Prod.fst}.$$$

Lean4

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

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru