comp_iff — Mathlib

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⟩

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