English
Two singles are equal if and only if either i=j and xi and xj are HEQ, or both are zero.
Русский
Два одиночных элемента равны тогда и только тогда, когда либо i=j и xi и xj равны в HEq, либо оба равны нулю.
LaTeX
$$$\mathrm{single}\ i\ xi = \mathrm{single}\ j\ xj \iff (i=j \land \xi \;\HEq\; xj) \lor (\xi = 0 \land xj = 0)$$$
Lean4
/-- Like `Finsupp.single_eq_single_iff`, but with a `HEq` due to dependent types -/
theorem single_eq_single_iff (i j : ι) (xi : β i) (xj : β j) :
DFinsupp.single i xi = DFinsupp.single j xj ↔ i = j ∧ xi ≍ xj ∨ xi = 0 ∧ xj = 0 :=
by
constructor
· intro h
by_cases hij : i = j
· subst hij
exact Or.inl ⟨rfl, heq_of_eq (DFinsupp.single_injective h)⟩
· have h_coe : ⇑(DFinsupp.single i xi) = DFinsupp.single j xj := congr_arg (⇑) h
have hci := congr_fun h_coe i
have hcj := congr_fun h_coe j
rw [DFinsupp.single_eq_same] at hci hcj
rw [DFinsupp.single_eq_of_ne hij] at hci
rw [DFinsupp.single_eq_of_ne (Ne.symm hij)] at hcj
exact Or.inr ⟨hci, hcj.symm⟩
· rintro (⟨rfl, hxi⟩ | ⟨hi, hj⟩)
· rw [eq_of_heq hxi]
· rw [hi, hj, DFinsupp.single_zero, DFinsupp.single_zero]
