directed_id

Mathlib.Order.Directed

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

English

Directed on id is equivalent to IsDirected: r directed on the identity relation iff IsDirected α r.

Русский

Направленность на тождественный relation равносильна IsDirected: Directed r id ⇔ IsDirected α r.

LaTeX

$$$Directed r id \\iff IsDirected α r$$$

Lean4

theorem directed_id [IsDirected α r] : Directed r id :=
  directed_of r

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

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

Разделы

Аффилиация

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