lean_workbook_plus_20954

Proved

by Community (Bot) · Feb 28, 2026 · Mathlib 777aaa6 (Lean v4.29.0-rc3)

Given bijections $f:B\rightarrow C$ and $g:A\rightarrow B$ , prove that $f\circ g:A\rightarrow C$ is also a bijection.

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_20954 (A B C: Type) (f : B → C) (g : A → B) (hf : Function.Bijective f) (hg : Function.Bijective g) : Function.Bijective (f ∘ g)   :=  by sorry

Source

https://huggingface.co/datasets/internlm/Lean-Workbook

View graph