English
TotallyBounded s iff for every filter f on α, if f is nontrivial and f ≤ principal s, there exists a subfilter c ≤ f which is Cauchy.
Русский
Полная ограниченность множества s эквивалентна существованию субфильтра, который тождественно меньше исходного и является Cauchy.
LaTeX
$$$$TotallyBounded(s) \\iff \\forall f, f.NeBot \\to f \\le \\mathrm{principal}(s) \\to \\exists c \\le f, Cauchy(c).$$$$
Lean4
theorem totallyBounded_iff_filter {s : Set α} : TotallyBounded s ↔ ∀ f, NeBot f → f ≤ 𝓟 s → ∃ c ≤ f, Cauchy c :=
by
constructor
·
exact fun H f hf hfs =>
⟨Ultrafilter.of f, Ultrafilter.of_le f,
(Ultrafilter.of f).cauchy_of_totallyBounded H ((Ultrafilter.of_le f).trans hfs)⟩
· intro H d hd
contrapose! H with hd_cover
set f := ⨅ t : Finset α, 𝓟 (s \ ⋃ y ∈ t, {x | (x, y) ∈ d})
have hb : HasAntitoneBasis f fun t : Finset α ↦ s \ ⋃ y ∈ t, {x | (x, y) ∈ d} :=
.iInf_principal fun _ _ ↦ diff_subset_diff_right ∘ biUnion_subset_biUnion_left
have : Filter.NeBot f := hb.1.neBot_iff.2 fun _ ↦ diff_nonempty.2 <| hd_cover _ (Finset.finite_toSet _)
have : f ≤ 𝓟 s := iInf_le_of_le ∅ (by simp)
refine ⟨f, ‹_›, ‹_›, fun c hcf hc => ?_⟩
rcases mem_prod_same_iff.1 (hc.2 hd) with ⟨m, hm, hmd⟩
rcases hc.1.nonempty_of_mem hm with ⟨y, hym⟩
have : s \ {x | (x, y) ∈ d} ∈ c := by simpa using hcf (hb.mem { y })
rcases hc.1.nonempty_of_mem (inter_mem hm this) with ⟨z, hzm, -, hyz⟩
exact hyz (hmd ⟨hzm, hym⟩)
