English
A variant of the choice-based Pi-induction that uses a maximal element chosen by a predicate.
Русский
Вариант индукции по Pi с выбором, который выбирает максимальный элемент по заданному предикату.
LaTeX
$$$\\text{induction\_on\_pi\_of\_choice} \\dots$$$
Lean4
/-- 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 `fun _ ↦ ∅` and for any function `g : ∀ i, Finset (α i)`, an index
`i : ι`, and an element`x : α 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 needs `x ∉ g i` and does not need `∀ i, LinearOrder (α i)`. -/
theorem induction_on_pi_max [∀ i, LinearOrder (α i)] {p : (∀ i, Finset (α i)) → Prop} (f : ∀ i, Finset (α i))
(h0 : p fun _ ↦ ∅)
(step : ∀ (g : ∀ i, Finset (α i)) (i : ι) (x : α i), (∀ y ∈ g i, y < x) → p g → p (update g i (insert x (g i)))) :
p f :=
induction_on_pi_of_choice (fun _ x s ↦ ∀ y ∈ s, y < x)
(fun _ s hs ↦ ⟨s.max' hs, s.max'_mem hs, fun _ ↦ s.lt_max'_of_mem_erase_max' _⟩) f h0 step
