compl

Mathlib.Order.Basic

URI: https://scilib.ai/kg/mathlib#IsIrrefl.compl

English

If r is irreflexive, then its complement rᶜ is reflexive.

Русский

Если r иррефлексивно, то его дополнение rᶜ рефлексивно.

LaTeX

$$$ [IsIrrefl\; \alpha\; r] \Rightarrow [IsRefl\; α\; r^{c}]$$$

Lean4

instance compl (r) [IsIrrefl α r] : IsRefl α rᶜ :=
  ⟨@irrefl α r _⟩

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

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

Разделы

Аффилиация

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