comp_eqToHom_lift_iff — Mathlib

English

For R,S in 𝒮 and a',a,b in 𝒳, f and φ with h : a' = a, p.IsHomLift f (inst.comp (eqToHom h) φ) is equivalent to p.IsHomLift f φ.

Русский

Для R,S в 𝒮 и a',a,b в 𝒳, f и φ с h : a' = a, p.IsHomLift f (comp (eqToHom h) φ) эквивалентно p.IsHomLift f φ.

LaTeX

$$$$ p.IsHomLift f (eqToHom h \; \circ \; \varphi) \; \Leftrightarrow \; p.IsHomLift f \; \varphi $$$$

Lean4

@[simp]
theorem comp_eqToHom_lift_iff {R S : 𝒮} {a' a b : 𝒳} (f : R ⟶ S) (φ : a ⟶ b) (h : a' = a) :
    p.IsHomLift f (eqToHom h ≫ φ) ↔ p.IsHomLift f φ
    where
  mp hφ' := by subst h; simpa using hφ'
  mpr _ := inferInstance

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