fst_comp_inl

Mathlib.Algebra.Order.Monoid.Lex

URI: https://scilib.ai/kg/mathlib#OrderMonoidHom.fst_comp_inl

English

The composition of the first projection with the inclusion inl is the identity on α: fst ∘ inl = id on α.

Русский

Композицией первой проекции с включением inl равна тождество на α: fst ∘ inl = id_α.

LaTeX

$$$$ fst_{\alpha,\beta} \circ inl_{\alpha,\beta} = \mathrm{id}_{\alpha}. $$$$

Lean4

@[to_additive (attr := simp)]
theorem fst_comp_inl : (fst α β).comp (inl α β) = .id α :=
  rfl

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

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

Разделы

Аффилиация

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