wellFounded_of_isEmpty

Mathlib.Logic.IsEmpty

URI: https://scilib.ai/kg/mathlib#wellFounded_of_isEmpty

English

If α is empty, then any relation r on α is WellFounded.

Русский

Если α пуст, тогда любая relation r на α исходит к WellFounded.

LaTeX

$$WellFounded r$$

Lean4

theorem wellFounded_of_isEmpty {α} [IsEmpty α] (r : α → α → Prop) : WellFounded r :=
  ⟨isEmptyElim⟩

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

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

Разделы

Аффилиация

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