lift_comp_of — Mathlib

English

The lift_comp_of identity expresses that the lift composed with the canonical injections recovers F.

Русский

lift_comp_of выражает, что подъём вместе с каноническими вводами восстанавливает исходное отображение F.

LaTeX

$$$\mathrm{lift\_comp\_of}(F) = F$$$

Lean4

@[simp]
theorem lift_comp_of (F : DirectLimit G f →+* P) :
    lift G f _ (fun i ↦ F.comp <| of G f i) (fun i j hij x ↦ by simp) = F := by ext; simp

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