extend_apply — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

theorem extend_apply {g : α → γ} (hf : g.FactorsThrough f) (e' : β → γ) (a : α) : extend f g e' (f a) = g a := by
  classical
  simp only [extend_def, dif_pos, exists_apply_eq_apply]
  exact hf (Classical.choose_spec (exists_apply_eq_apply f a))

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