no goals
𝕜 : Type u_1
E : Type ?u.282167
F : Type ?u.282170
β : Type ?u.282173
inst✝ : LinearOrderedField 𝕜
s : Set 𝕜
⊢ Convex 𝕜 s ↔ OrdConnected s
simp_rw [convex_iff_segment_subset, segment_eq_uIcc, ordConnected_iff_uIcc_subset]