fuzzy_irrefl

Mathlib.SetTheory.PGame.Order

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

English

No game is fuzzy with itself: for all x, not x ‖ x.

Русский

Ни одна игра не является fuzzy самой с собой: для всех x, не x ‖ x.

LaTeX

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

Lean4

theorem fuzzy_irrefl (x : PGame) : ¬x ‖ x := fun h => lf_irrefl x h.1

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

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

Разделы

Аффилиация

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