lift_of' — Mathlib

English

Compatibility of lifts with composition shows that lifting respects composition of the component maps.

Русский

Совместимость подъёмов с композициями показывает, что подъем сохраняет композицию компонент.

LaTeX

$$$(\mathrm{lift} \circ \text{comp})(i) = \text{comp} \circ (\mathrm{lift} i)$$$

Lean4

@[simp]
theorem lift_of' : lift G f _ (of G f) (fun i j hij x ↦ by simp) = .id _ := by ext; simp

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