extend_comp — Mathlib

English

If g factors through f, then extend (f23 ∘ f12) g e' = extend f23 (extend f12 g (e' ∘ f23)) e'.

Русский

Если g факторизуется через f, тогда extend через композицию сохраняется: extend (f23 ∘ f12) g e' = extend f23 (extend f12 g (e' ∘ f23)) e'.

LaTeX

$$$\operatorname{extend} (f_{23} \circ f_{12})\ g\ e' = \operatorname{extend} f_{23} (\operatorname{extend} f_{12} g (e' \circ f_{23})) e'$$$

Lean4

theorem extend_comp {g : α → γ} (e' : β → γ) (hf : FactorsThrough g f) : extend f g e' ∘ f = g :=
  funext fun a => hf.extend_apply e' a

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