Description: Completeness of a Hilbert space. (Contributed by NM, 8-Sep-2007) (Revised by Mario Carneiro, 9-May-2014) (New usage is discouraged.)