comp_injective — Mathlib

English

Injectivity is preserved under composition with an embedding; i.e., e ∘ f is injective iff f is.

Русский

Инъективность сохраняется при композиции с вложением: e ∘ f инъективно тогда и только тогда, когда f инъективен.

LaTeX

$$$\forall {F} {f:\, \alpha \to \beta} {e:\, E}, \ \operatorname{Injective}(e \circ f) \iff \operatorname{Injective} f.$$$

Lean4

@[simp]
theorem comp_injective {F : Sort*} [FunLike F β γ] [EmbeddingLike F β γ] (f : α → β) (e : F) :
    Function.Injective (e ∘ f) ↔ Function.Injective f :=
  (EmbeddingLike.injective e).of_comp_iff f

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