Theorems · Theorem · combinatorics

Finset.update_piecewise

∀ {ι : Type u_1} {π : ι → Sort u_2} (s : Finset ι) (f g : (i : ι) → π i) [inst : (j : ι) → Decidable (j ∈ s)]
  [inst_1 : DecidableEq ι] (i : ι) (v : π i),
  Function.update (s.piecewise f g) i v = s.piecewise (Function.update f i v) (Function.update g i v)

Defined in

Mathlib.Data.Finset.Piecewise

Cited by

2 results in Mathlib

Foundations

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

Assumes

DecidableDecidableEq