single_eq_of_sigma_eq — Mathlib

English

If ⟨i, xi⟩ = ⟨j, xj⟩ in the Sigma type, then single i xi = single j xj.

Русский

Если пары ⟨i, xi⟩ и ⟨j, xj⟩ равны в суммарном типе (Sigma), тогда одиночные элементы равны.

LaTeX

$$$\langle i, \xi \rangle = \langle j, x_j \rangle \Rightarrow \mathrm{single}\ i\ \xi = \mathrm{single}\ j\ x_j$$$

Lean4

/-- Equality of sigma types is sufficient (but not necessary) to show equality of `DFinsupp`s. -/
theorem single_eq_of_sigma_eq {i j} {xi : β i} {xj : β j} (h : (⟨i, xi⟩ : Sigma β) = ⟨j, xj⟩) :
    DFinsupp.single i xi = DFinsupp.single j xj := by
  cases h
  rfl

Похожие утверждения