directedOn_pair'

Mathlib.Order.Directed

URI: https://scilib.ai/kg/mathlib#directedOn_pair'

← MathLib Explorer

English

If {b,a} is the same as {a,b}, then DirectedOn r ({b, a}) holds by symmetry.

Русский

Если множество {b,a} совпадает с {a,b}, то DirectedOn выполняется по симметрии.

LaTeX

$$$\text{DirectedOn}(r, \{b,a\})$$$

Lean4

theorem directedOn_pair' (h : Reflexive r) {a b : α} (hab : a ≼ b) : DirectedOn r ({ b, a } : Set α) :=
  by
  rw [Set.pair_comm]
  apply directedOn_pair h hab

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

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

Разделы

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

Аффилиация

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