English
Let α be a type and f be an injective function on α. Then the underlying map x ↦ f(x) is injective.
Русский
Пусть α — множество, f — инъективная функция на α. Тогда отображение x ↦ f(x) инъективно.
LaTeX
$$$\forall f:\text{InjectiveFunction}(\alpha),\; \text{Injective}(\lambda x:\alpha, f\,x)$$$
Lean4
protected theorem injective [DecidableEq α] (f : InjectiveFunction α) : Injective (apply f) :=
by
obtain ⟨xs, hperm, hnodup⟩ := f
generalize h₀ : List.map Sigma.fst xs = xs₀
generalize h₁ : xs.map (@id ((Σ _ : α, α) → α) <| @Sigma.snd α fun _ : α => α) = xs₁
dsimp [id] at h₁
have hxs : xs = TotalFunction.List.toFinmap' (xs₀.zip xs₁) :=
by
rw [← h₀, ← h₁, List.toFinmap']; clear h₀ h₁ xs₀ xs₁ hperm hnodup
induction xs with
| nil => simp only [List.zip_nil_right, List.map_nil]
| cons xs_hd xs_tl
xs_ih =>
simp only [Sigma.eta, List.zip_cons_cons, List.map, List.cons_inj_right]
exact xs_ih
revert hperm hnodup
rw [hxs]; intro hperm hnodup
apply InjectiveFunction.applyId_injective
· rwa [← h₀, hxs, hperm.nodup_iff]
· rwa [← hxs, h₀, h₁] at hperm
