English
If f is injOn on s, then InjOn (g ∘ f) s holds iff InjOn g (f '' s) holds.
Русский
Если f инъективна на s, то InjOn (g ∘ f) s эквивалентно InjOn g (f '' s).
LaTeX
$$$ \\operatorname{InjOn} f s \\Rightarrow (\\operatorname{InjOn}(g \\circ f) s \\iff \\operatorname{InjOn} g (f'' s))$$$
Lean4
theorem comp_iff (hf : InjOn f s) : InjOn (g ∘ f) s ↔ InjOn g (f '' s) :=
⟨image_of_comp, fun h ↦ InjOn.comp h hf <| mapsTo_image f s⟩