uncurry_single — Mathlib

English

The uncurry of a singleton on indices a,b with value m is the singleton on the pair (a,b) with value m: (single a (single b m)).uncurry = single (a,b) m.

Русский

Раскаррирование одиночной функции: (single a (single b m)).uncurry = single (a,b) m.

LaTeX

$$$(\mathrm{single}\ a\ (\mathrm{single}\ b\ m)).uncurry = \mathrm{single} (a,b) m$$$

Lean4

@[simp]
theorem uncurry_single (a : α) (b : β) (m : M) : (single a (single b m)).uncurry = single (a, b) m :=
  by
  ext ⟨x, y⟩
  rcases eq_or_ne a x with rfl | hne <;> classical simp [single_apply, *]

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