acc_zero — Mathlib

English

The zero element is accessible for the Lex order on DFinsupp provided the stability condition prevents any s-step from mapping to zero.

Русский

Элемент ноль под порядком Lex на DFinsupp является доступным, если условие стабильности исключает переход к нулю по операции s.

LaTeX

$$$\\mathrm{acc\\_zero}:\\ Acc(DFinsupp.Lex(r,s))\\ 0$ with the hypothesis \\ (hbot:\\forall i a, \\neg s(i,a,0))$$

Lean4

theorem acc_zero (hbot : ∀ ⦃i a⦄, ¬s i a 0) : Acc (DFinsupp.Lex r s) 0 :=
  Acc.intro 0 fun _ ⟨_, _, h⟩ => (hbot h).elim

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