wellFoundedLT_of_finite — Mathlib

English

If a single coordinate i has acc under a certain order, then the dependent function that is nonzero only at i has acc under Lex.

Русский

Если одна координата i имеет acc под заданным порядком, то зависимая функция, ненулевая только на i, имеет acc по Lex.

LaTeX

$$$\\forall i,\\ Acc (r^c\\cap(\\cdot \\neq \\cdot)) i \\Rightarrow \\forall a,\\ Acc(DFinsupp.Lex(r,s)) (single\\ i\\ a)$$$

Lean4

instance wellFoundedLT_of_finite [LinearOrder ι] [Finite ι] [∀ i, Zero (α i)] [∀ i, LT (α i)]
    [hwf : ∀ i, WellFoundedLT (α i)] : WellFoundedLT (Lex (Π₀ i, α i)) :=
  ⟨DFinsupp.Lex.wellFounded_of_finite (· < ·) fun i => (hwf i).1⟩

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