casesOn' — Mathlib

English

The elimination principle for PartENat: to prove a property for all a, it suffices to prove it for ⊤ and for all some n.

Русский

Принцип разборa по PartENat: чтобы доказать свойство для любого a, достаточно доказать его для ⊤ и для каждого some n.

LaTeX

$$@[elab_as_elim] protected theorem casesOn' {P : PartENat → Prop} : ∀ a : PartENat, P ⊤ → (∀ n : ℕ, P (some n)) → P a$$

Lean4

@[elab_as_elim]
protected theorem casesOn' {P : PartENat → Prop} : ∀ a : PartENat, P ⊤ → (∀ n : ℕ, P (some n)) → P a :=
  Part.induction_on

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