comp_eqToHom_lift — Mathlib

English

For R,S in 𝒮, a,b in 𝒳, the lift of φ by f is equivalent to the lift of φ by eqToHom composition with f, i.e., p.IsHomLift f (eqToHom (comp h) φ) ↔ p.IsHomLift f φ.

Русский

Для R,S в 𝒮; a,b в 𝒳; подъем φ над f равносилен подъему φ над eqToHom(композиции) с f: p.IsHomLift f (eqToHom (comp h) φ) ⇔ p.IsHomLift f φ.

LaTeX

$$$$ p.IsHomLift f (eqToHom (comp (eqToHom h) \; φ)) \Leftrightarrow p.IsHomLift f φ $$$$

Lean4

instance comp_eqToHom_lift {a' : 𝒳} (h : a' = a) : p.IsHomLift f (eqToHom h ≫ φ) := by subst h; simp_all

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