fac_lift — Mathlib

English

Another formulation of lift_mk_comp, stating the same equality with potentially different assumptions on f,g and their images.

Русский

Еще одна формулировка lift_mk_comp, выражающая то же равенство с возможными разными предпосылками на f, g и их образы.

LaTeX

$$$\text{Same as above: } \text{lift}_{f,g} = \mathrm{image.\,ι}(f \circ g).$$$

Lean4

@[reassoc (attr := simp)]
theorem fac_lift (F' : MonoFactorisation f) : factorThruImage f ≫ image.lift F' = F'.e :=
  (Image.isImage f).fac_lift F'

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