wellFounded

Mathlib.Data.Finsupp.WellFounded

URI: https://scilib.ai/kg/mathlib#Finsupp.Lex.wellFounded

← MathLib Explorer

English

If hbot, hs, and hr hold, then Finsupp.Lex r s is well-founded.

Русский

Если выполняются hbot, hs и hr, то Finsupp.Lex r s является хорошо основанной.

LaTeX

$$$WellFounded (Finsupp.Lex r s)$$$

Lean4

theorem wellFounded (hbot : ∀ ⦃n⦄, ¬s n 0) (hs : WellFounded s) (hr : WellFounded <| rᶜ ⊓ (· ≠ ·)) :
    WellFounded (Finsupp.Lex r s) :=
  ⟨fun x => Lex.acc hbot hs x fun a _ => hr.apply a⟩

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

Научная платформа российской исследовательской школы.

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru