instIsIrreflSetOfProdMatch_1PropOfIsIrrefl

Mathlib.Data.Rel

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

English

If R is irreflexive on α, then the relation on α×α given by {(a,b) | R a b} is irrefl.

Русский

Если R иррефлексивно на α, то отношение на α×α, заданное {(a,b) | R a b}, иррефлексиво.

LaTeX

$$$\text{IsIrrefl } (\{(a,b) \mid R a b\})$$$

Lean4

instance {R : α → α → Prop} [IsIrrefl α R] : SetRel.IsIrrefl {(a, b) | R a b} :=
  ‹_›

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

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

Разделы

Аффилиация

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