@[reducible, inline]

abbrev Nary.Func (n : ℕ) (α : Type u_1) (β : Sort u_2) : Sort (imax (u_1 + 1) u_2)

Equations

• Nary.Func n α β = (Vector α n → β)

def Nary.IndependentOf {n : ℕ} {α : Type u_1} {β : Sort u_2} (f : Func n α β) (i : Fin n) : Prop

IndependentOf f i if the output of f does not depend on the value of the ith input.

Equations

• Nary.IndependentOf f i = ∀ (a : α) (v : Vector α n), f v = f (v.set (↑i) a ⋯)

def Nary.DependsOn {n : ℕ} {α : Type u_1} {β : Sort u_2} (f : Func n α β) (i : Fin n) : Prop

DependsOn f i if the output of f depends on the value of the ith input.

Equations

• Nary.DependsOn f i = ¬Nary.IndependentOf f i

def Nary.Dependency {n : ℕ} {α : Type u_1} {β : Sort u_2} (f : Func n α β) : Type

The type of indices that a given function depends on.

Equations

• Nary.Dependency f = { i : Fin n // Nary.DependsOn f i }

theorem Nary.eq_of_forall_dependency_getElem_eq {n : ℕ} {α : Type u_1} {β : Sort u_2} {f : Func n α β} {I J : Vector α n} : (∀ (x : Dependency f), I[↑x] = J[↑x]) → f I = f J

def Nary.restrict {n : ℕ} {α : Type u_1} {β : Sort u_2} (f : Func n α β) : α → Fin n → Func n α β

Equations

• Nary.restrict f a i I = f (I.set (↑i) a ⋯)

@[simp]

theorem Nary.restrict_const {β✝ : Sort u_1} {b : β✝} {α✝ : Type u_2} {c : α✝} {n✝ : ℕ} {i : Fin n✝} : restrict (Function.const (Vector α✝ n✝) b) c i = Function.const (Vector α✝ n✝) b

theorem Nary.restrict_independentOf {n✝ : ℕ} {α✝ : Type u_1} {β✝ : Sort u_2} {f : Func n✝ α✝ β✝} {c : α✝} {i : Fin n✝} : IndependentOf (restrict f c i) i