α : Type u_1
inst✝ : LinearOrder α
r : α
s : Finset α
⊢ ¬toColex s < toColex {r} ↔ ∃ x, x ∈ s ∧ ¬x < r
α : Type u_1
inst✝ : LinearOrder α
r : α
s : Finset α
⊢ toColex {r} ≤ toColex s ↔ ∃ x, x ∈ s ∧ r ≤ x
simp only [← not_lt]
no goals
α : Type u_1
inst✝ : LinearOrder α
r : α
s : Finset α
⊢ ¬toColex s < toColex {r} ↔ ∃ x, x ∈ s ∧ ¬x < r
simp [lt_singleton_iff_mem_lt]