Theorems · Theorem

DependsOn.updateFinset

∀ {ι : Type u_2} {π : ι → Type u_3} [inst : DecidableEq ι] {α : Type u_1} {f : ((i : ι) → π i) → α} {s : Set ι},
  DependsOn f s → ∀ {t : Finset ι} (y : (i : ↥t) → π ↑i), DependsOn (fun x => f (Function.updateFinset x t y)) (s \ ↑t)

If one replaces the variables indexed by a finite set t, then f no longer depends on those variables.

Defined in

Mathlib.Data.Finset.Update

Cited by

2 results in Mathlib

Foundations

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

Assumes

DecidableEq