surjective_comp_right' — Mathlib

English

There exists an extension witness making g ∘ f equal to any given h, showing surjectivity of the right composition map.

Русский

Существование доказательства существования соответствия, доказывающее сюрьективность правого отображения.

LaTeX

$$$\text{Surjective} (\lambda g: \beta \to \gamma.\ g \circ f)$$$

Lean4

theorem surjective_comp_right' (hf : Injective f) (g₀ : β → γ) : Surjective fun g : β → γ ↦ g ∘ f := fun g ↦
  ⟨extend f g g₀, Function.extend_comp hf _ _⟩

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