English
Let α, β, γ be types and g : β → γ be a bijection. Then the map on functions h : α → β given by h ↦ g ∘ h is a bijection from α → β to α → γ.
Русский
Пусть $\alpha$, $\beta$, $\gamma$ — множества, а $g: \beta \to \gamma$ биекция. Тогда отображение на множества функций $h: \alpha \to \beta$, заданное $h \mapsto g \circ h$, является биекцией между $\alpha \to \beta$ и $\alpha \to \gamma$.
LaTeX
$$$\\operatorname{Bij}(\\,g \\circ \\cdot\\,: (\\alpha \\to \\beta) \\to (\\alpha \\to \\gamma)\\)$$$
Lean4
/-- Composition by a bijective function on the left is itself bijective. -/
theorem comp_left {g : β → γ} (hg : Bijective g) : Bijective (g ∘ · : (α → β) → α → γ) :=
⟨hg.injective.comp_left, hg.surjective.comp_left⟩
