injective_iff — Mathlib

English

Let h be InjOn g s and hs range f ⊆ s. Then Injective (g ∘ f) iff Injective f.

Русский

Пусть h — InjOn g s и hs: range f ⊆ s. Тогда Injective (g ∘ f) эквивалентно Injective f.

LaTeX

$$$ [\\operatorname{InjOn} g s] (\\operatorname{range} f \\subseteq s) \\Rightarrow (\\operatorname{Injective}(g \\circ f) \\iff \\operatorname{Injective}(f))$$$

Lean4

theorem _root_.Set.InjOn.injective_iff (s : Set β) (h : InjOn g s) (hs : range f ⊆ s) :
    Injective (g ∘ f) ↔ Injective f :=
  ⟨(·.of_comp), fun h _ ↦ by aesop⟩

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