sbtw_irrefl

Mathlib.Order.Circular

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

English

For all a, not sbtw a a a.

Русский

Для всех a: не sbtw a a a.

LaTeX

$$$\\forall a:\\alpha,\\ ¬sbtw(a,a,a)$$$

Lean4

theorem sbtw_irrefl (a : α) : ¬sbtw a a a :=
  sbtw_irrefl_left_right

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

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

Разделы

Аффилиация

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