lift_base — Mathlib

English

Evaluating lift on base φ yields k.

Русский

Просмотр lift на базовой карте φ дает k.

LaTeX

$$$(lift(f,k,hf))(base(φ)(h)) = k(h)$ for all h ∈ H$$

Lean4

@[simp]
theorem lift_base (f : ∀ i, G i →* K) (k : H →* K) (hf : ∀ i, (f i).comp (φ i) = k) (g : H) :
    (lift f k hf) (base φ g : PushoutI φ) = k g :=
  by
  delta PushoutI lift base
  simp only [MonoidHom.coe_comp, Con.coe_mk', comp_apply, Con.lift_coe, lift_apply_inr]
    -- `ext` attribute should be lower priority then `hom_ext_nonempty`

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