liftOn_zero — Mathlib

English

Let f be a function f: M → S → P with a compatibility hypothesis H. Then the lift of the zero element in the localization satisfies liftOn 0 f H = f 0 1; i.e., the lifted value at zero equals the value of f at (0,1).

Русский

Пусть f: M → S → P с условием совместимости H. Тогда лифтинг нуля в локализации удовлетворяет liftOn 0 f H = f 0 1; т. е. значение лифтинга в нуле равно значению f в (0,1).

LaTeX

$$$\mathrm{liftOn}\,0\,f\,H = f\,0\,1$$$

Lean4

theorem liftOn_zero {p : Type*} (f : M → S → p) (H) : liftOn 0 f H = f 0 1 := by rw [← mk_zero 1, liftOn_mk]

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