no goals
α : Type u
β : Type v
r✝ : α → α → Prop
s✝ : β → β → Prop
r : α → α → Prop
s : Set α
⊢ ¬Bounded r s ↔ Unbounded r s
simp only [Bounded, Unbounded, not_forall, not_exists, exists_prop, not_and, not_not]