English
If f is injective on s, then bijectivity of g∘f on s to p is equivalent to bijectivity of g on the image of f on s to p.
Русский
Если f инъективна на s, то биективность g∘f на s к p эквивалентна биективности g на изображении f(s) к p.
LaTeX
$$$\\text{InjOn}(f,s) \\Rightarrow (\\text{BijOn}(g\\circ f,s,p) \\iff \\text{BijOn}(g, f''s, p))$$$
Lean4
/-- If `f : α → β` and `g : β → γ` and if `f` is injective on `s`, then `f ∘ g` is a bijection
on `s` iff `g` is a bijection on `f '' s`. -/
theorem bijOn_comp_iff (hf : InjOn f s) : BijOn (g ∘ f) s p ↔ BijOn g (f '' s) p := by
simp only [BijOn, InjOn.comp_iff, surjOn_comp_iff, mapsTo_image_iff, hf]
