irrefl

Mathlib.Data.Rel

URI: https://scilib.ai/kg/mathlib#SetRel.irrefl

English

If R is irrefl, then no element is related to itself: ¬ a ~[R] a for every a.

Русский

Если R иррефлексивно, то ни одно a не связано с самим собой: ¬ a ~_R a для любого a.

LaTeX

$$$\forall a, \neg a ~[R] a$$$

Lean4

protected theorem irrefl [R.IsIrrefl] : ¬a ~[R] a :=
  irrefl_of (· ~[R] ·) _

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

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

Разделы

Аффилиация

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