directed

Mathlib.Order.Directed

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

← MathLib Explorer

English

If IsTotal α r, then r is a directed relation (IsDirected).

Русский

Если r разомротен (IsTotal), тогда r является направленным отношением (IsDirected).

LaTeX

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

Lean4

theorem directed [IsTotal α r] (f : ι → α) : Directed r f := fun i j =>
  Or.casesOn (total_of r (f i) (f j)) (fun h => ⟨j, h, refl _⟩) fun h => ⟨i, refl _, h⟩

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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