Finset.induction_on_pi_min
theorem Finset.induction_on_pi_min :
∀ {ι : Type u_1} {α : ι → Type u_2} [inst : Finite ι] [inst : DecidableEq ι] [inst_1 : (i : ι) → DecidableEq (α i)]
[inst_2 : (i : ι) → LinearOrder (α i)] {p : ((i : ι) → Finset (α i)) → Prop} (f : (i : ι) → Finset (α i)),
(p fun x => ∅) →
(∀ (g : (i : ι) → Finset (α i)) (i : ι) (x : α i),
(∀ y ∈ g i, x < y) → p g → p (Function.update g i (insert x (g i)))) →
p f
This theorem, `Finset.induction_on_pi_min`, states that for any finite type `ι` and any type `α` indexed by `ι` with the property of decidable equality and a linear order, for any predicate `p` on functions from `ι` to the sets of `α i`, if `p` holds for the function that maps every element to the empty set, and if for any function `g` from `ι` to the sets of `α i`, any index `i : ι`, and any element `x : α i` that is strictly less than all elements of `g i`, `p g` implies `p (Function.update g i (insert x (g i)))`, then `p` holds for all such functions. In simpler terms, it provides a basis for induction on functions that map an index set to finite sets, under the condition that a new element is always strictly smaller than existing elements.
More concisely: Given a finite type `ι`, a type `α` indexed by `ι` with decidable equality and a linear order, and a predicate `p` on functions from `ι` to sets of `α i`, if `p` holds for the constant function mapping every index to the empty set and `p g` implies `p (Function.update g i (insert x (g i)))` for all `g : ι → set α i`, `i : ι`, and `x : α i` strictly less than all elements of `g i`, then `p` holds for all such functions.
|
Finset.induction_on_pi_of_choice
theorem Finset.induction_on_pi_of_choice :
∀ {ι : Type u_1} {α : ι → Type u_2} [inst : Finite ι] [inst : DecidableEq ι] [inst_1 : (i : ι) → DecidableEq (α i)]
(r : (i : ι) → α i → Finset (α i) → Prop),
(∀ (i : ι) (s : Finset (α i)), s.Nonempty → ∃ x ∈ s, r i x (s.erase x)) →
∀ {p : ((i : ι) → Finset (α i)) → Prop} (f : (i : ι) → Finset (α i)),
(p fun x => ∅) →
(∀ (g : (i : ι) → Finset (α i)) (i : ι) (x : α i),
r i x (g i) → p g → p (Function.update g i (insert x (g i)))) →
p f
The theorem `Finset.induction_on_pi_of_choice` establishes a generalized induction principle for finite sets in the form of `Finset.induction_on_pi`. It is parameterized over types `ι` and `α`, which are indexed by `ι`. The types `ι` and `α` are assumed to be finite and equipped with decidable equality. The theorem takes a relation `r` defined on each index `i` of `ι`, an element `x` from the set at index `i`, and a finite set of `α` at index `i`.
The theorem states that if for every index `i` and any nonempty finite set `s` on `α` at index `i`, there exists an element `x` in `s` such that relation `r` holds for `i`, `x` and the finite set obtained by erasing `x` from `s`, then for any predicate `p` over functions mapping from `ι` to finite sets on `α`, and any such function `f`, if `p` holds for the function that returns an empty set for every input, and if `p` can be extended from any function `g`, index `i`, and an element `x` for which `r` holds and `p` holds for `g` to the function obtained by replacing the value of `g` at `i` with the set obtained by inserting `x` into `g i`, then `p` must hold for `f`.
More concisely: If for every index `i` and finite set `s` on `α`, there exists an `x` in `s` such that `r(i, x, s \ {x})` holds, then a predicate `p` holds for any function `f` if it holds for the constant function to the empty set and can be extended along `r` through any index and element.
|
Finset.induction_on_pi_max
theorem Finset.induction_on_pi_max :
∀ {ι : Type u_1} {α : ι → Type u_2} [inst : Finite ι] [inst : DecidableEq ι] [inst_1 : (i : ι) → DecidableEq (α i)]
[inst_2 : (i : ι) → LinearOrder (α i)] {p : ((i : ι) → Finset (α i)) → Prop} (f : (i : ι) → Finset (α i)),
(p fun x => ∅) →
(∀ (g : (i : ι) → Finset (α i)) (i : ι) (x : α i),
(∀ y ∈ g i, y < x) → p g → p (Function.update g i (insert x (g i)))) →
p f
The theorem `Finset.induction_on_pi_max` states that for a finite type `ι` and a function `α` that maps each index `ι` to a type, under the conditions that each `α i` follows a linear order and each `ι` and `α i` has decidable equality, we can prove a predicate `p` holds for all functions `f` mapping `ι` to a finite set `Finset (α i)` if two conditions are met. First, `p` holds for a function that maps every index to an empty set. Second, for any function `g`, index `i`, and element `x` in `α i` that is strictly larger than all elements in `g i`, if `p g` holds, then `p` also holds after updating `g i` with the set obtained by inserting `x` into `g i`. The proof of this theorem is omitted.
More concisely: Given a finite type `ι` and a function `α : ι → Type`, if each `α i` has a linear order with decidable equality, then a predicate `p : (ι → Finset α) → Prop` holds for all functions `f : ι → Finset α` if it holds for the empty function and for any `i` and `x > α i.max f i`, `p` also holds after updating `f i` with the insertion of `x`.
|
Finset.induction_on_pi
theorem Finset.induction_on_pi :
∀ {ι : Type u_1} {α : ι → Type u_2} [inst : Finite ι] [inst : DecidableEq ι] [inst_1 : (i : ι) → DecidableEq (α i)]
{p : ((i : ι) → Finset (α i)) → Prop} (f : (i : ι) → Finset (α i)),
(p fun x => ∅) →
(∀ (g : (i : ι) → Finset (α i)) (i : ι), ∀ x ∉ g i, p g → p (Function.update g i (insert x (g i)))) → p f
This theorem, `Finset.induction_on_pi`, is about the property of a predicate on functions of type `∀ i, Finset (α i)` where `α` is defined on a finite type `ι`. It asserts that if the predicate is true when applied to a function that maps everything to the empty set, and if the predicate remains true when a new element `x` not already in the image of an index `i` under a function `g` is inserted into the image of `i` under `g`, then the predicate holds for all such functions. This theorem is useful for establishing properties of functions defined on finite sets, and there are specialized versions of this theorem for cases where `∀ i, LinearOrder (α i)`.
More concisely: If a predicate holds for all functions mapping a finite type to sets, when applied to the constant function to the empty set and when extended by mapping a new element to an index not in the image, then it holds for all such functions.
|