liftOfLE_apply

Mathlib.Algebra.Module.LocalizedModule.Basic

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

English

Applying liftOfLE to f1 x yields f2 x for any x in M.

Русский

При применении liftOfLE к f1 x получаем f2 x для любого x ∈ M.

LaTeX

$$$$ \\text{liftOfLE}(f_1 x) = f_2 x $$$$

Lean4

@[simp]
theorem liftOfLE_apply (x) : liftOfLE S₁ S₂ h f₁ f₂ (f₁ x) = f₂ x :=
  lift_apply ..

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

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

Разделы

Аффилиация

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