lift_comp_inr

Mathlib.GroupTheory.SemidirectProduct

URI: https://scilib.ai/kg/mathlib#SemidirectProduct.lift_comp_inr

English

The lift map composed with inr equals inr composed with fg.

Русский

Составление lift с inr равен inr вместе с fg.

LaTeX

$$$ (lift(fn)(fg)(h)) \circ inr = inr(\,fg\, ) $$$

Lean4

@[simp]
theorem lift_comp_inr : (lift fn fg h).comp inr = fg := by ext; simp

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

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

Разделы

Аффилиация

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