totallyBounded_iff_ultrafilter — Mathlib

English

TotallyBounded s iff for every ultrafilter f on α, f ≤ principal s implies Cauchy f.

Русский

TotallyBounded s эквивалентно тому, что для каждого ультрафильтра f на α, если f ≤ principal s, то f полноценно Cauchy.

LaTeX

$$$$TotallyBounded(s) \\iff \\forall f : Ultrafilter(\\alpha), f \\leqslant \\mathrm{principal}(s) \\Rightarrow Cauchy(f).$$$$

Lean4

theorem totallyBounded_iff_ultrafilter {s : Set α} :
    TotallyBounded s ↔ ∀ f : Ultrafilter α, ↑f ≤ 𝓟 s → Cauchy (f : Filter α) :=
  by
  refine ⟨fun hs f => f.cauchy_of_totallyBounded hs, fun H => totallyBounded_iff_filter.2 ?_⟩
  intro f hf hfs
  exact ⟨Ultrafilter.of f, Ultrafilter.of_le f, H _ ((Ultrafilter.of_le f).trans hfs)⟩

Похожие утверждения