Theorems · Theorem · order theory

directedOn_pair

∀ {α : Type u_1} {r : α → α → Prop} [Std.Refl r] {a b : α}, r a b → DirectedOn r {a, b}

Defined in

Mathlib.Order.Directed

Cited by

2 results in Mathlib

Foundations

Depth 8 from the axioms · uses no axioms

Assumes

Std.Refl