Gro-Tsen
The definition of a Cauchy sequence (u_n) is: (★) ∀ε>0. ∃n. ∀p,q≥n. |u_p − u_q| < ε But it can also be given as: (☆) ∀ε>0. ∃n. ∀r≥n. |u_r − u_n| < ε This seems a bit simpler, if less symmetric. Is there some reason nobody ever seems to write it that way?