lift_apply_apply — Mathlib

English

There is a concrete description of the lift: it is determined by the base map f and the nilpotent perturbation e via the formula above.

Русский

Согласно описанию лифта, он задаётся базовым отображением f и нилпотентной помехой e через приведённую формулу.

LaTeX

$$$\text{lift } fe\; a = fe.1 a. fst + fe.1 a.snd \cdot fe.2,$$$

Lean4

theorem lift_apply_apply (fe : { _fe : (A →ₐ[R] B) × B // _ }) (a : A[ε]) :
    lift fe a = fe.val.1 a.fst + fe.val.1 a.snd * fe.val.2 :=
  rfl

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