induction_on_fintype_pi — Mathlib

English

Recursion/induction principle for quotients indexed by a finite type; reduction to a simpler case via finite structure.

Русский

Рекурсивная индукция по фактор-объектам, индексируемым конечным типом; сведение к более простой структуре.

LaTeX

$$$\\forall q, C q \\leftarrow \\text{ind_fintype_pi}$$$

Lean4

/-- Choice-free induction principle for quotients indexed by a finite type.
  See `Quotient.induction_on_pi` for the general version assuming `Classical.choice`. -/
@[elab_as_elim]
theorem induction_on_fintype_pi {C : (∀ i, Quotient (S i)) → Prop} (q : ∀ i, Quotient (S i))
    (f : ∀ a : ∀ i, α i, C (⟦a ·⟧)) : C q :=
  ind_fintype_pi f q

Похожие утверждения