instIsIrreflOfIsWellFounded

Mathlib.Order.RelClasses

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

English

If a relation r on α is well-founded, then it is irreflexive.

Русский

Если отношение r на множестве α хорошо основано, то оно иррефлексивно.

LaTeX

$$$[\text{IsWellFounded } \alpha\ r] \Rightarrow IsIrrefl(\alpha, r)$$$

Lean4

instance (priority := 100) (r : α → α → Prop) [IsWellFounded α r] : IsIrrefl α r :=
  IsAsymm.isIrrefl

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

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

Разделы

Аффилиация

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