comp_injective — Mathlib

English

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

Русский

Для функции f и эквивалентности e — композиция через e инъективна тогда и только тогда, когда f инъективна.

LaTeX

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

Lean4

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

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