directedOn_univ_iff

Mathlib.Order.Directed

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

← MathLib Explorer

English

DirectedOn r Set.univ is equivalent to IsDirected α r.

Русский

DirectedOn r Set.univ эквивалентно IsDirected α r.

LaTeX

$$$DirectedOn\\ r\\ Set.univ \\iff IsDirected α r$$$

Lean4

theorem directedOn_univ_iff : DirectedOn r Set.univ ↔ IsDirected α r :=
  ⟨fun h =>
    ⟨fun a b =>
      let ⟨c, _, hc⟩ := h a trivial b trivial
      ⟨c, hc⟩⟩,
    @directedOn_univ _ _⟩
    -- see Note [lower instance priority]

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

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

Разделы

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

Аффилиация

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