Theorems · Theorem

Function.updateFinset_updateFinset

∀ {ι : Type u_1} {π : ι → Type u_2} {x : (i : ι) → π i} [inst : DecidableEq ι] {s t : Finset ι} {y : (i : ↥s) → π ↑i}
  {z : (i : ↥t) → π ↑i} (hst : Disjoint s t),
  Function.updateFinset (Function.updateFinset x s y) t z =
    Function.updateFinset x (s ∪ t) ((Equiv.piFinsetUnion π hst) (y, z))

Defined in

Mathlib.Data.Finset.Update

Cited by

2 results in Mathlib

Foundations

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

Assumes

DecidableEq