lift_ι_apply — Mathlib

English

The symmetric application property of lift confirms the same equality as ι_comp_lift but in equivalent form.

Русский

Симметричная версия применения lift подтверждает то же равенство, что и ι_comp_lift, в эквивалентной форме.

LaTeX

$$lift_symm_apply : (lift R f).symm F = (F : UniversalEnvelopingAlgebra R L →ₗ⁅R⁆ A).comp (ι R)$$

Lean4

theorem lift_ι_apply (x : L) : lift R f (ι R x) = f x := by
  rw [← Function.comp_apply (f := lift R f) (g := ι R) (x := x), ι_comp_lift]

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