totallyBounded_Icc — Mathlib

English

For all a,b ∈ ℚ, the closed interval Icc(a,b) is totally bounded in the metric on ℚ.

Русский

Для любых a,b \\in \\mathbb{Q} множество [a,b] totally bounded.

LaTeX

$$$\\forall a,b \\in \\mathbb{Q}, \\operatorname{TotallyBounded}(\\mathrm{Icc}(a,b))$$$

Lean4

nonrec theorem totallyBounded_Icc (a b : ℚ) : TotallyBounded (Icc a b) := by
  simpa only [preimage_cast_Icc] using
    totallyBounded_preimage Rat.isUniformEmbedding_coe_real.isUniformInducing (totallyBounded_Icc (a : ℝ) b)

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