coe_liftRight — Mathlib

English

For any f, g with hx, the coefficient of liftRight at x equals f x; i.e., (liftRight f g h x) = g x and its underlying equals f x.

Русский

Для любых f, g с условием h, коэффициент liftRight в точке x равен f x; то есть (liftRight f g h x) = f x.

LaTeX

$$$ (liftRight\\;f\\;g\\;h\\;x : N) = f\\;x $$$

Lean4

@[to_additive (attr := simp)]
theorem coe_liftRight {f : M →* N} {g : M → Nˣ} (h : ∀ x, ↑(g x) = f x) (x) : (liftRight f g h x : N) = f x :=
  h x

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