injective_comp_right_iff_surjective

English

For any type γ that is nontrivial, the map that sends g: β → γ to g ∘ f is injective if and only if f is surjective.

Русский

Если γ ненулевого типа, то отображение g: β → γ, заданное g ↦ g ∘ f, инъективно тогда и только тогда, когда f сюръективна.

LaTeX

$$$\\text{Injective}(g \\mapsto g\\circ f) \\iff \\text{Surjective}(f)$$$

Lean4

theorem injective_comp_right_iff_surjective {γ : Type*} [Nontrivial γ] :
    Injective (fun g : β → γ ↦ g ∘ f) ↔ Surjective f :=
  by
  refine ⟨not_imp_not.mp fun not_surj inj ↦ not_subsingleton γ ⟨fun c c' ↦ ?_⟩, (·.injective_comp_right)⟩
  have ⟨b₀, hb⟩ := not_forall.mp not_surj
  classical have := inj (a₁ := fun _ ↦ c) (a₂ := (if · = b₀ then c' else c)) ?_
  · simpa using congr_fun this b₀
  ext a; simp only [comp_apply, if_neg fun h ↦ hb ⟨a, h⟩]

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