injective_comp_left_iff — Mathlib

English

If f is injective, then Injective (f ∘ g) iff Injective g.

Русский

Если f инъективна, то Injective (f ∘ g) эквивалентно Injective g.

LaTeX

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

Lean4

theorem injective_comp_left_iff [Nonempty α] {g : β → γ} : Injective (g ∘ · : (α → β) → α → γ) ↔ Injective g :=
  ⟨fun h b₁ b₂ eq ↦ Nonempty.elim ‹_› (congr_fun <| h (a₁ := fun _ ↦ b₁) (a₂ := fun _ ↦ b₂) <| funext fun _ ↦ eq),
    (·.comp_left)⟩

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