coe_fst

Mathlib.LinearAlgebra.AffineSpace.AffineMap

URI: https://scilib.ai/kg/mathlib#AffineMap.coe_fst

English

The coe of fst equals Prod.fst, i.e., the embedding preserves the standard projection.

Русский

Сопоставление коe fst равно Prod.fst, то есть вложение сохраняет стандартную проекцию.

LaTeX

$$$$\mathrm{coe}(fst) = \mathrm{Prod}.fst$$$$

Lean4

@[simp]
theorem coe_fst : ⇑(fst : P1 × P2 →ᵃ[k] P1) = Prod.fst :=
  rfl

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

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

Разделы

Аффилиация

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