The least set a function depends on

Lemmas on mathlib's DependsOn. The sets a function depends on are closed under binary intersection, so a function that depends on a finite set depends on a least one: the coordinates it does not ignore, those at which changing the argument alone can change the value.

Closure under infinite intersections fails. A function of a set of natural numbers that says whether the set is infinite depends exactly on the cofinite sets, and they have no least element.

Main results

• DependsOn.inter: a function that depends on s and on t depends on s ∩ t.
• dependsOn_compl_singleton_iff: a function ignores a coordinate when updating it never changes the value.
• isLeast_dependsOn: a function that depends on a finite set depends on the coordinates it does not ignore, and these lie in every set it depends on.

theorem DependsOn.inter {ι : Type u_1} {α : ι → Type u_2} {β : Type u_3} {f : ((i : ι) → α i) → β} {s t : Set ι} (hs : DependsOn f s) (ht : DependsOn f t) : DependsOn f (s ∩ t)

A function that depends on s and on t depends on s ∩ t.

theorem DependsOn.biInter {ι : Type u_1} {α : ι → Type u_2} {β : Type u_3} {f : ((i : ι) → α i) → β} {κ : Type u_4} {u : Set κ} (hu : u.Finite) {t : κ → Set ι} (h : ∀ k ∈ u, DependsOn f (t k)) : DependsOn f (⋂ k ∈ u, t k)

A function that depends on each of finitely many sets depends on their intersection.

theorem dependsOn_compl_singleton_iff {ι : Type u_1} {α : ι → Type u_2} {β : Type u_3} {f : ((i : ι) → α i) → β} [DecidableEq ι] {i : ι} : DependsOn f {i}ᶜ ↔ ∀ (x : (a : ι) → α a) (a : α i), f (Function.update x i a) = f x

A function ignores the coordinate i when updating it never changes the value.

theorem isLeast_dependsOn {ι : Type u_1} {α : ι → Type u_2} {β : Type u_3} {f : ((i : ι) → α i) → β} {s : Set ι} (hs : s.Finite) (hf : DependsOn f s) : IsLeast {t : Set ι | DependsOn f t} {i : ι | ¬DependsOn f {i}ᶜ}

A function that depends on a finite set depends on the coordinates it does not ignore, and every set it depends on contains them.

theorem isLeast_dependsOn_of_finite {ι : Type u_1} {α : ι → Type u_2} {β : Type u_3} [Finite ι] (f : ((i : ι) → α i) → β) : IsLeast {t : Set ι | DependsOn f t} {i : ι | ¬DependsOn f {i}ᶜ}

A function of finitely many coordinates depends on the coordinates it does not ignore, and every set it depends on contains them.