Theorems · Theorem · combinatorics

Finset.piecewise_insert

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

Defined in

Mathlib.Data.Finset.Piecewise

Cited by

6 results in Mathlib

Foundations

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

Assumes

DecidableDecidableEqDecidable