# Documentation

Mathlib.Data.Finset.PiInduction

# Induction principles for ∀ i, Finset (α i)∀ i, Finset (α i)#

In this file we prove a few induction principles for functions Π i : ι, Finset (α i) defined on a finite type.

• Finset.induction_on_pi is a generic lemma that requires only [Finite ι], [DecidableEq ι], and [∀ i, DecidableEq (α i)]∀ i, DecidableEq (α i)]; this version can be seen as a direct generalization of Finset.induction_on.

• Finset.induction_on_pi_max and Finset.induction_on_pi_min: generalizations of Finset.induction_on_max; these versions require ∀ i, LinearOrder (α i)∀ i, LinearOrder (α i) but assume ∀ y ∈ g i, y < x∀ y ∈ g i, y < x∈ g i, y < x and ∀ y ∈ g i, x < y∀ y ∈ g i, x < y∈ g i, x < y respectively in the induction step.

## Tags #

finite set, finite type, induction, function

theorem Finset.induction_on_pi_of_choice {ι : Type u_2} {α : ιType u_1} [inst : ] [inst : ] [inst : (i : ι) → DecidableEq (α i)] (r : (i : ι) → α iFinset (α i)Prop) (H_ex : ∀ (i : ι) (s : Finset (α i)), x, x s r i x ()) {p : ((i : ι) → Finset (α i)) → Prop} (f : (i : ι) → Finset (α i)) (h0 : p fun x => ) (step : (g : (i : ι) → Finset (α i)) → (i : ι) → (x : α i) → r i x (g i)p gp (Function.update g i (insert x (g i)))) :
p f

General theorem for Finset.induction_on_pi-style induction principles.

theorem Finset.induction_on_pi {ι : Type u_2} {α : ιType u_1} [inst : ] [inst : ] [inst : (i : ι) → DecidableEq (α i)] {p : ((i : ι) → Finset (α i)) → Prop} (f : (i : ι) → Finset (α i)) (h0 : p fun x => ) (step : (g : (i : ι) → Finset (α i)) → (i : ι) → (x : α i) → ¬x g ip gp (Function.update g i (insert x (g i)))) :
p f

Given a predicate on functions ∀ i, Finset (α i)∀ i, Finset (α i) defined on a finite type, it is true on all maps provided that it is true on fun _ ↦ ∅↦ ∅∅ and for any function g : ∀ i, Finset (α i)∀ i, Finset (α i), an index i : ι, and x ∉ g i∉ g i, p g implies p (update g i (insert x (g i))).

See also Finset.induction_on_pi_max and Finset.induction_on_pi_min for specialized versions that require ∀ i, LinearOrder (α i)∀ i, LinearOrder (α i).

theorem Finset.induction_on_pi_max {ι : Type u_2} {α : ιType u_1} [inst : ] [inst : ] [inst : (i : ι) → DecidableEq (α i)] [inst : (i : ι) → LinearOrder (α i)] {p : ((i : ι) → Finset (α i)) → Prop} (f : (i : ι) → Finset (α i)) (h0 : p fun x => ) (step : (g : (i : ι) → Finset (α i)) → (i : ι) → (x : α i) → (∀ (y : α i), y g iy < x) → p gp (Function.update g i (insert x (g i)))) :
p f

Given a predicate on functions ∀ i, Finset (α i)∀ i, Finset (α i) defined on a finite type, it is true on all maps provided that it is true on fun _ ↦ ∅↦ ∅∅ and for any function g : ∀ i, Finset (α i)∀ i, Finset (α i), an index i : ι, and an elementx : α i that is strictly greater than all elements of g i, p g implies p (update g i (insert x (g i))).

This lemma requires LinearOrder instances on all α i. See also Finset.induction_on_pi for a version that x ∉ g i∉ g i instead of does not need∀ i, LinearOrder (α i).

theorem Finset.induction_on_pi_min {ι : Type u_2} {α : ιType u_1} [inst : ] [inst : ] [inst : (i : ι) → DecidableEq (α i)] [inst : (i : ι) → LinearOrder (α i)] {p : ((i : ι) → Finset (α i)) → Prop} (f : (i : ι) → Finset (α i)) (h0 : p fun x => ) (step : (g : (i : ι) → Finset (α i)) → (i : ι) → (x : α i) → (∀ (y : α i), y g ix < y) → p gp (Function.update g i (insert x (g i)))) :
p f

Given a predicate on functions ∀ i, Finset (α i)∀ i, Finset (α i) defined on a finite type, it is true on all maps provided that it is true on fun _ ↦ ∅↦ ∅∅ and for any function g : ∀ i, Finset (α i)∀ i, Finset (α i), an index i : ι, and an elementx : α i that is strictly less than all elements of g i, p g implies p (update g i (insert x (g i))).

This lemma requires LinearOrder instances on all α i. See also Finset.induction_on_pi for a version that x ∉ g i∉ g i instead of does not need∀ i, LinearOrder (α i).