Theorems · Theorem · order theory

Set.unbounded_inter_not

∀ {α : Type u_1} {r : α → α → Prop} {s : Set α},
  (∀ (a b : α), ∃ m, ∀ (c : α), r c a ∨ r c b → r c m) →
    ∀ (a : α), Set.Unbounded r (s ∩ {b | ¬r b a}) ↔ Set.Unbounded r s

Defined in

Mathlib.Order.Bounded

Cited by

0 results in Mathlib

Foundations

Depth 16 from the axioms · uses propext, Classical.choice, Quot.sound