Composite_of_Bijections_is_Bijection
Provedbijectionscomposite-mappingsproofwiki
If f and g are both bijections, then so is f ∘ g.
Preamble
import Mathlib.Logic.Function.Basic
Formal statement
theorem Composite_of_Bijections_is_Bijection {α β γ : Type _} {f : β → γ} {g : α → β} (hf : Function.Bijective f) (hg : Function.Bijective g) : Function.Bijective (f ∘ g) := by sorrySource