injective_comp — Mathlib

English

Equiv.injective_comp: For e : α ≃ β and f : β → γ, Injective (f ∘ e) ↔ Injective f.

Русский

Инъективность композиции с эквивалентностью эквивалентно инъективности функции f: Injective (f ∘ e) ⇔ Injective f.

LaTeX

$$Injective\\left( f \\circ e \\right) \\iff Injective\\left( f \\right)$$

Lean4

theorem injective_comp (e : α ≃ β) (f : β → γ) : Injective (f ∘ e) ↔ Injective f :=
  EquivLike.injective_comp e f

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