lift_unique — Mathlib

English

If F is a map from the direct limit to P, then F equals the lift composed with injections on every component.

Русский

Если F есть отображение из прямого предела в P, то F совпадает с lift, когда ограничено на каждую компоненту.

LaTeX

$$$F = \mathrm{lift}(G,f,P,g,Hg) \text{ on all injections }\iota_i$$$

Lean4

@[deprecated lift_comp_of (since := "2025-08-11")]
theorem lift_unique (F : DirectLimit G f →+ P) (x) :
    F x = lift G f P (fun i ↦ F.comp (of G f i)) (fun i j hij x ↦ by simp) x := by rw [lift_comp_of]

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