instIsIrreflRel

Mathlib.Order.WellFounded

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

English

If α has a well-founded relation, then the corresponding WellFoundedRelation.rel is irreflexive.

Русский

Если у множества есть хорошо основанное отношение, то соответствующее отношение WellFoundedRelation.rel иррефлексивно.

LaTeX

$$$IsIrrefl\ α\ WellFoundedRelation.rel$$$

Lean4

instance : IsIrrefl α WellFoundedRelation.rel :=
  IsAsymm.isIrrefl

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

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

Разделы

Аффилиация

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