lift_of — Mathlib

English

The value of lift on generators is compatible: lift(f, k, hf)(of i g) = f_i(g).

Русский

Значение lift на генераторах совместимо: lift(f,k,hf)(of_i(g)) = f_i(g).

LaTeX

$$$lift(f,k,hf)(of_i(g)) = f_i(g)$$$

Lean4

@[simp]
theorem lift_of (f : ∀ i, G i →* K) (k : H →* K) (hf : ∀ i, (f i).comp (φ i) = k) {i : ι} (g : G i) :
    (lift f k hf) (of i g : PushoutI φ) = f i g :=
  by
  delta PushoutI lift of
  simp only [MonoidHom.coe_comp, Con.coe_mk', comp_apply, Con.lift_coe, lift_apply_inl, CoprodI.lift_of]

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