fst_comp_toSigma

Mathlib.Data.Sigma.Basic

URI: https://scilib.ai/kg/mathlib#Prod.fst_comp_toSigma

English

The composition of Sigma.fst with Prod.toSigma equals Prod.fst.

Русский

Составление Sigma.fst с Prod.toSigma равно Prod.fst.

LaTeX

$$$\\mathrm{Sigma.fst} \\circ \\mathrm{Prod.toSigma} = \\mathrm{Prod.fst}$$$

Lean4

@[simp]
theorem fst_comp_toSigma {α β} : Sigma.fst ∘ @Prod.toSigma α β = Prod.fst :=
  rfl

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

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

Разделы

Аффилиация

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