Theorems · Theorem · general algebraic systems

DFinsupp.sigmaUncurry_single

∀ {ι : Type u} {α : ι → Type u_2} {δ : (i : ι) → α i → Type v} [inst : DecidableEq ι]
  [inst_1 : (i : ι) → (j : α i) → Zero (δ i j)] [inst_2 : (i : ι) → DecidableEq (α i)] (i : ι) (j : α i) (x : δ i j),
  (fun₀ | i => fun₀ | j => x).sigmaUncurry = fun₀ | ⟨i, j⟩ => x

Defined in

Mathlib.Data.DFinsupp.Sigma

Cited by

0 results in Mathlib

Foundations

Depth 77 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

DecidableEqZeroDecidableEq