comp_right — Mathlib

English

If h: FactorsThrough g f, then g ∘ g' factors through f ∘ g'.

Русский

Если g факторизуется через f, то g ∘ g' факторизуется через f ∘ g'.

LaTeX

$$$\text{FactorsThrough } g f \rightarrow \text{FactorsThrough } (g \circ g') (f \circ g')$$$

Lean4

theorem comp_right {α β γ δ : Sort*} {f : α → β} {g : α → γ} (h : FactorsThrough g f) (g' : δ → α) :
    FactorsThrough (g ∘ g') (f ∘ g') := fun _x _y hxy ↦ h hxy

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