instIsIrreflLF

Mathlib.SetTheory.PGame.Order

URI: https://scilib.ai/kg/mathlib#SetTheory.PGame.instIsIrreflLF

English

The relation LF on PGame is irreflexive.

Русский

Отношение LF на PGame иррефлексивно.

LaTeX

$$$$ \\forall x, \\neg x \\;LF\\; x. $$$$

Lean4

instance : IsIrrefl _ (· ⧏ ·) :=
  ⟨lf_irrefl⟩

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

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

Разделы

Аффилиация

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