English
If univ is complete then the space is complete; conversely, if the space is complete then univ is complete.
Русский
Если вселенная полна, то пространство полно; наоборот, если пространство полно, то вселенная полна.
LaTeX
$$$IsComplete(univ) \\iff CompleteSpace(\\alpha)$$$
Lean4
/-- A Cauchy filter in a discrete uniform space is contained in the principal filter
of a point. -/
theorem eq_pure_of_cauchy {f : Filter α} (hf : Cauchy f) : ∃ x : α, f = pure x :=
by
rcases hf with ⟨f_ne_bot, f_le⟩
simp only [DiscreteUniformity.eq_principal_idRel, le_principal_iff, mem_prod_iff] at f_le
obtain ⟨S, ⟨hS, ⟨T, ⟨hT, H⟩⟩⟩⟩ := f_le
obtain ⟨x, rfl⟩ := eq_singleton_left_of_prod_subset_idRel (f_ne_bot.nonempty_of_mem hS) (Filter.nonempty_of_mem hT) H
exact ⟨x, f_ne_bot.le_pure_iff.mp <| le_pure_iff.mpr hS⟩
