of_fac — Mathlib

English

Let R,S ∈ 𝒮 and a,b ∈ 𝒳 with ha: p.obj a = R, hb: p.obj b = S. If h : f = eqToHom ha.symm ≫ p.map φ ≫ eqToHom hb, then p.IsHomLift f φ.

Русский

Пусть R,S ∈ 𝒮 и a,b ∈ 𝒳 с ha: p.obj a = R, hb: p.obj b = S. Если f совпадает с выражением ha.symm, затем p.map φ и hb, то есть f = eqToHom ha.symm ≫ p.map φ ≫ eqToHom hb, то φ является подъемом над f.

LaTeX

$$$$ f = \mathrm{eqToHom}(ha^{\mathrm{symm}}) \; \gg \; p.map(\varphi) \; \gg \; \mathrm{eqToHom}(hb) $$ implies $$ p.IsHomLift f \; \varphi $$$$

Lean4

theorem of_fac {R S : 𝒮} {a b : 𝒳} (f : R ⟶ S) (φ : a ⟶ b) (ha : p.obj a = R) (hb : p.obj b = S)
    (h : f = eqToHom ha.symm ≫ p.map φ ≫ eqToHom hb) : p.IsHomLift f φ := by subst ha hb h; simp

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