English
Let f be a function from the product indexed by ι to β, and let s be a subset of ι. We say that f depends on s if whenever two inputs x and y agree on all coordinates in s, we have f(x) = f(y).
Русский
Пусть f: Π i, α i → β — функция, заданная на произведении индексов i, и пусть s ⊆ ι. Говорят, что f зависит от s, если для любых x,y с x i = y i для всех i ∈ s выполняется f(x) = f(y).
LaTeX
$$$DependsOn(f,s) \iff \forall x,y:\; (\forall i \in s,\; x(i)=y(i)) \rightarrow f(x)=f(y)$$$
Lean4
/-- A function `f` depends on `s` if, whenever `x` and `y` coincide over `s`, `f x = f y`.
It should be interpreted as "`f` _potentially_ depends only on variables in `s`".
However it might be the case that `f` does not depend at all on variables in `s`,
for example if `f` is constant. As a consequence, `DependsOn f univ` is always true,
see `dependsOn_univ`. -/
def DependsOn (f : (Π i, α i) → β) (s : Set ι) : Prop :=
∀ ⦃x y⦄, (∀ i ∈ s, x i = y i) → f x = f y
