lift_inl

Mathlib.GroupTheory.SemidirectProduct

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

English

In the lift construction, the image of inl(n) is fn(n).

Русский

В конструировании lift образ inl(n) равен fn(n).

LaTeX

$$$ lift\_inl : lift(fn)(fg)(h)(inl(n)) = fn(n) $$$

Lean4

@[simp]
theorem lift_inl (n : N) : lift fn fg h (inl n) = fn n := by simp [lift]

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

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

Разделы

Аффилиация

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