totallyBounded_range — Mathlib

English

Every Cauchy sequence s : ℕ → α has a totally bounded range.

Русский

Каждая последовательность Коши s : ℕ → α имеет полностью ограниченное множество значений (образ).

LaTeX

$$$\text{CauchySeq}(s) \Rightarrow \operatorname{TotallyBounded}(\operatorname{range}(s))$$$

Lean4

/-- Every Cauchy sequence over `ℕ` is totally bounded. -/
theorem totallyBounded_range {s : ℕ → α} (hs : CauchySeq s) : TotallyBounded (range s) :=
  by
  intro a ha
  obtain ⟨n, hn⟩ := cauchySeq_iff.1 hs a ha
  refine ⟨s '' {k | k ≤ n}, (finite_le_nat _).image _, ?_⟩
  rw [range_subset_iff, biUnion_image]
  intro m
  rw [mem_iUnion₂]
  rcases le_total m n with hm | hm
  exacts [⟨m, hm, refl_mem_uniformity ha⟩, ⟨n, le_refl n, hn m hm n le_rfl⟩]

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