induction_on_all_not — Mathlib

English

Induction principle on the prenex structure: if Prelim conditions hold, then P φ.

Русский

Индукция по структуре пренекс: если выполнены предпосылки, то P φ.

LaTeX

$$$\forall P\, [IsPrenex(\varphi) \Rightarrow (\dots) \Rightarrow P(\varphi)]$$$

Lean4

theorem induction_on_all_not {P : ∀ {n}, L.BoundedFormula α n → Prop} {φ : L.BoundedFormula α n} (h : IsPrenex φ)
    (hq : ∀ {m} {ψ : L.BoundedFormula α m}, ψ.IsQF → P ψ) (ha : ∀ {m} {ψ : L.BoundedFormula α (m + 1)}, P ψ → P ψ.all)
    (hn : ∀ {m} {ψ : L.BoundedFormula α m}, P ψ → P ψ.not) : P φ :=
  IsPrenex.recOn h hq (fun _ => ha) fun _ ih => hn (ha (hn ih))

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