Theorems · Theorem · order theory

DirectedOn.insert

∀ {α : Type u_1} {r : α → α → Prop} [Std.Refl r] (a : α) {s : Set α},
  DirectedOn r s → (∀ b ∈ s, ∃ c ∈ s, r a c ∧ r b c) → DirectedOn r (insert a s)

Defined in

Mathlib.Order.Directed

Cited by

1 results in Mathlib

Foundations

Depth 7 from the axioms · uses no axioms

Assumes

Std.Refl