instIsIrreflFuzzy

Mathlib.SetTheory.PGame.Order

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

English

The fuzzy relation is irreflexive, i.e., for every x, not x ‖ x.

Русский

Отношение fuzzy иррефлексивно: для каждого x не x ‖ x.

LaTeX

$$$\forall x\in \mathrm{PGame},\; \neg (x \|\| x)$$$

Lean4

instance : IsIrrefl _ (· ‖ ·) :=
  ⟨fuzzy_irrefl⟩

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

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

Разделы

Аффилиация

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