to_isDirected

Mathlib.Order.Directed

URI: https://scilib.ai/kg/mathlib#IsTotal.to_isDirected

English

If IsTotal α r, then IsDirected α r. This shows totality implies directedness.

Русский

Если IsTotal α r, то IsDirected α r. Это показывает, что тотальность порождает направленность.

LaTeX

$$$[IsTotal\\ α\\ r] \\Rightarrow IsDirected α r$$$

Lean4

instance (priority := 100) to_isDirected [IsTotal α r] : IsDirected α r :=
  directed_id_iff.1 <| IsTotal.directed _

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

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

Разделы

Аффилиация

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