injOn_range — Mathlib

English

If g ∘ f is injective, then g is injective on range f.

Русский

Если g ∘ f инъективна, то g инъективна на образе f.

LaTeX

$$$ \\operatorname{Injective}(\\operatorname{Function}.compose g f) \\Rightarrow \\operatorname{InjOn} g (\\operatorname{range} f)$$$

Lean4

theorem _root_.Function.Injective.injOn_range (h : Injective (g ∘ f)) : InjOn g (range f) :=
  by
  rintro _ ⟨x, rfl⟩ _ ⟨y, rfl⟩ H
  exact congr_arg f (h H)

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