English
If fγ is injective, then the elimination function elim γ fγ is injective as a function from WType β to γ.
Русский
Если fγ инъективна, то эллиминационная функция elim γ fγ инъективна по отношению к WType β.
LaTeX
$$$\text{If } f_\gamma \text{ is injective, then } WType.elim\;\gamma\;f_\gamma \text{ is injective.}$$$
Lean4
theorem elim_injective (γ : Type*) (fγ : (Σ a : α, β a → γ) → γ) (fγ_injective : Function.Injective fγ) :
Function.Injective (elim γ fγ)
| ⟨a₁, f₁⟩, ⟨a₂, f₂⟩, h => by
obtain ⟨rfl, h⟩ := Sigma.mk.inj_iff.mp (fγ_injective h)
congr with x
exact elim_injective γ fγ fγ_injective (congr_fun (eq_of_heq h) x :)
