induction_on — Mathlib

English

Every Finmap can be built from a finite-alist representation; if a property holds for every a in AList β, then it holds for all Finmap β.

Русский

Любое Finmap β можно представить через AList β; если свойство выполняется для каждого a : AList β, то оно выполняется для любого Finmap β.

LaTeX

$$$$ \forall s : Finmap \beta,$ \forall a : AList \beta, C(a.toFinmap) \Rightarrow C(s) $ $$$$

Lean4

@[elab_as_elim]
theorem induction_on {C : Finmap β → Prop} (s : Finmap β) (H : ∀ a : AList β, C ⟦a⟧) : C s := by rcases s with ⟨⟨a⟩, h⟩;
  exact H ⟨a, h⟩

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