English
If all α i are linearly ordered, there is a Pi-induction principle using minimal elements instead of maximal ones.
Русский
Если все множества α i линейно упорядочены, существует принцип индукции по Pi с использованием минимальных элементов.
LaTeX
$$$\\text{induction\_on\_pi\_min} \\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 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 needs `x ∉ g i` and does not need `∀ i, LinearOrder (α i)`. -/
theorem induction_on_pi_min [∀ 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, x < y) → p g → p (update g i (insert x (g i)))) :
p f :=
induction_on_pi_max (α := fun i ↦ (α i)ᵒᵈ) _ h0 step
