# mathlibdocumentation

data.finset.pi_induction

# Induction principles for Π 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 [fintype ι], [decidable_eq ι], and [Π i, decidable_eq (α 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, linear_order (α i) but assume ∀ y ∈ g i, y < x and ∀ 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_1} {α : ι → Type u_2} [fintype ι] [decidable_eq ι] [Π (i : ι), decidable_eq (α i)] (r : Π (i : ι), α ifinset (α i) → Prop) (H_ex : ∀ (i : ι) (s : finset (α i)), s.nonempty(∃ (x : α i) (H : x s), r i x (s.erase x))) {p : (Π (i : ι), finset (α i)) → Prop} (f : Π (i : ι), finset (α i)) (h0 : p (λ (_x : ι), )) (step : ∀ (g : Π (i : ι), finset (α i)) (i : ι) (x : α i), r i x (g i)p gp i (insert x (g i)))) :
p f

General theorem for finset.induction_on_pi-style induction principles.

theorem finset.induction_on_pi {ι : Type u_1} {α : ι → Type u_2} [fintype ι] [decidable_eq ι] [Π (i : ι), decidable_eq (α i)] {p : (Π (i : ι), finset (α i)) → Prop} (f : Π (i : ι), finset (α i)) (h0 : p (λ (_x : ι), )) (step : ∀ (g : Π (i : ι), finset (α i)) (i : ι) (x : α i), x g ip gp i (insert x (g i)))) :
p f

Given a predicate on functions Π i, finset (α i) defined on a finite type, it is true on all maps provided that it is true on λ _, ∅ and for any function g : Π i, finset (α i), an index i : ι, and x ∉ 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, linear_order (α i).

theorem finset.induction_on_pi_max {ι : Type u_1} {α : ι → Type u_2} [fintype ι] [decidable_eq ι] [Π (i : ι), decidable_eq (α i)] [Π (i : ι), linear_order (α i)] {p : (Π (i : ι), finset (α i)) → Prop} (f : Π (i : ι), finset (α i)) (h0 : p (λ (_x : ι), )) (step : ∀ (g : Π (i : ι), finset (α i)) (i : ι) (x : α i), (∀ (y : α i), y g iy < x)p gp i (insert x (g i)))) :
p f

Given a predicate on functions Π i, finset (α i) defined on a finite type, it is true on all maps provided that it is true on λ _, ∅ and for any function g : Π 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 linear_order instances on all α i. See also finset.induction_on_pi for a version that x ∉ g i instead of does not needΠ i, linear_order (α i).

theorem finset.induction_on_pi_min {ι : Type u_1} {α : ι → Type u_2} [fintype ι] [decidable_eq ι] [Π (i : ι), decidable_eq (α i)] [Π (i : ι), linear_order (α i)] {p : (Π (i : ι), finset (α i)) → Prop} (f : Π (i : ι), finset (α i)) (h0 : p (λ (_x : ι), )) (step : ∀ (g : Π (i : ι), finset (α i)) (i : ι) (x : α i), (∀ (y : α i), y g ix < y)p gp i (insert x (g i)))) :
p f

Given a predicate on functions Π i, finset (α i) defined on a finite type, it is true on all maps provided that it is true on λ _, ∅ and for any function g : Π 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 linear_order instances on all α i. See also finset.induction_on_pi for a version that x ∉ g i instead of does not needΠ i, linear_order (α i).