injective_comp — Mathlib

English

The injectivity of a composition corresponds to the injectivity of the inner function: f ∘ e is injective iff f is.

Русский

Инъективность композиции соответствует инъективности внутренней функции: f ∘ e инъективно ⇔ f инъективен.

LaTeX

$$$\forall {α,β,γ}, \operatorname{Injective}(f \circ e) \iff \operatorname{Injective}(f).$$$

Lean4

@[simp]
theorem injective_comp (e : E) (f : β → γ) : Function.Injective (f ∘ e) ↔ Function.Injective f :=
  Function.Injective.of_comp_iff' f (EquivLike.bijective e)

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