English
The embedding embSigma_n is injective: if embSigma_n(p) = embSigma_n(q) for p and q in the appropriate sigma-type, then p = q componentwise.
Русский
Отображение embSigma_n инъективно: если для двух элементов из соответствующего сигма-типа выполняется равенство embSigma_n(p) = embSigma_n(q), то p = q по всем компонентам.
LaTeX
$$$\\operatorname{Injective}(\\mathrm{embSigma}_n)$$$
Lean4
theorem injective_embSigma (n : ℕ) : Injective (embSigma n) :=
by
rintro ⟨plength, psize, -, pemb, -, -, -, -⟩ ⟨qlength, qsize, -, qemb, -, -, -, -⟩
intro hpq
simp_all only [Sigma.mk.inj_iff, true_and, mk.injEq, Fin.mk.injEq, embSigma]
have : plength = qlength := hpq.1
subst this
simp_all only [Sigma.mk.inj_iff, heq_eq_eq, true_and, and_true]
ext i
exact
mk.inj_iff.mp
(congr_fun hpq.1 i)
/- The best proof would probably to establish the bijection with Finpartitions, but we opt
for a direct argument, embedding `OrderedPartition n` in a type which is obviously finite. -/
