casesOn — Mathlib

English

The standard elimination principle for PartENat: for any P, ∀ a, P ⊤ → ∀ n, P n.cast → P a.

Русский

Стандартный принцип устранения для PartENat: для любого P верно, что если P(⊤) и P(n.cast) для всех n, тогда P(a).

LaTeX

$$part casesOn: {P : PartENat → Prop} : ∀ a : PartENat, P ⊤ → (∀ n : ℕ, P n.cast) → P a$$

Lean4

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

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