liftOfLE_comp

Mathlib.Algebra.Module.LocalizedModule.Basic

URI: https://scilib.ai/kg/mathlib#IsLocalizedModule.liftOfLE_comp

English

The composition with f1 preserves f2: (LiftOfLE S1 S2 h f1 f2) ∘ f1 = f2.

Русский

Композиция с f1 сохраняет f2: (LiftOfLE S1 S2 h f1 f2) ∘ f1 = f2.

LaTeX

$$$$ (\\text{LiftOfLE } S_1 S_2\; h\; f_1\\; f_2) \\circ f_1 = f_2 $$$$

Lean4

theorem liftOfLE_comp : (liftOfLE S₁ S₂ h f₁ f₂).comp f₁ = f₂ :=
  lift_comp ..

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

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

Разделы

Аффилиация

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