directed_of

Mathlib.Order.Directed

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

English

If r is a directed relation on α, then for any a,b ∈ α there exists c ∈ α with r a c and r b c.

Русский

Если r направлено, то для любых a,b ∈ α существует c ∈ α such that r a c и r b c.

LaTeX

$$$\\forall a,b \\in α, \\\\exists c, r a c \\\\land r b c$$$

Lean4

theorem directed_of (r : α → α → Prop) [IsDirected α r] (a b : α) : ∃ c, r a c ∧ r b c :=
  IsDirected.directed _ _

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

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

Разделы

Аффилиация

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