wellFoundedLT — Mathlib

English

If α is linearly ordered and WellFoundedGT α holds, then DegLex(α →₀ ℕ) equipped with the LT relation has WellFoundedLT.

Русский

При наличии линейного порядка на α и WellFoundedGT α, DegLex(α →₀ ℕ) с LT-порядком имеет WellFoundedLT.

LaTeX

$$$\text{WellFoundedLT}\left(\mathrm{DegLex}(\alpha \to\_0 \mathbb{N})\right)$$$

Lean4

instance wellFoundedLT [WellFoundedGT α] : WellFoundedLT (DegLex (α →₀ ℕ)) :=
  ⟨wellFounded wellFounded_gt wellFounded_lt fun n ↦ (zero_le n).not_gt⟩

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