psigma_skipLeft

Mathlib.Order.RelClasses

URI: https://scilib.ai/kg/mathlib#WellFounded.psigma_skipLeft

← MathLib Explorer

English

Skipping a left component preserves well-foundedness in PSigma.

Русский

Пропуск левого компонента сохраняет хорошо основанность в PSigma.

LaTeX

$$$[\\text{WellFounded } s] \\Rightarrow \\text{WellFounded } (PSigma.SkipLeft \\alpha s)$$$

Lean4

theorem psigma_skipLeft (α : Type u) {β : Type v} {s : β → β → Prop} (hb : WellFounded s) :
    WellFounded (SkipLeft α s) :=
  psigma_revLex emptyWf.wf hb

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

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

Разделы

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

Аффилиация

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