Theorems · Theorem · order theory

Set.bounded_inter_not

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

Defined in

Mathlib.Order.Bounded

Cited by

3 results in Mathlib

Foundations

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