factorsThrough_iff — Mathlib

English

g factors through f if and only if there exists e: β → γ with g = e ∘ f.

Русский

g факторизуется через f тогда и только тогда, когда существует e: β → γ с g = e ∘ f.

LaTeX

$$$g\ \text{factors through } f \iff \exists e:\beta \to \gamma,\ g = e \circ f$$$

Lean4

theorem factorsThrough_iff (g : α → γ) [Nonempty γ] : g.FactorsThrough f ↔ ∃ (e : β → γ), g = e ∘ f :=
  ⟨fun hf =>
    ⟨extend f g (const β (Classical.arbitrary γ)), funext (fun x => by simp only [comp_apply, hf.extend_apply])⟩,
    fun h _ _ hf => by rw [Classical.choose_spec h, comp_apply, comp_apply, hf]⟩

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