totallyBounded_iff_subset_finite_iUnion_nhds_one

English

A set s is totally bounded iff for every neighborhood U of identity, there exists a finite set t such that s is contained in the union over y in t of yU.

Русский

Множество s полностью ограничено тогда и только тогда, когда для каждой окрестности U единицы существует конечное множество t такое, что s ⊆ ⋃_{y∈t} yU.

LaTeX

$$$TotallyBounded(s) \\iff ∀ U ∈ 𝓝(1), ∃ t, t\\text{ finite} ∧ s \\subseteq \\bigcup_{y\\in t} y U$$$

Lean4

@[to_additive]
theorem totallyBounded_iff_subset_finite_iUnion_nhds_one {s : Set α} :
    TotallyBounded s ↔ ∀ U ∈ 𝓝 (1 : α), ∃ t : Set α, t.Finite ∧ s ⊆ ⋃ y ∈ t, y • U :=
  (𝓝 (1 : α)).basis_sets.uniformity_of_nhds_one_inv_mul_swapped.totallyBounded_iff.trans <| by
    simp [← preimage_smul_inv, preimage]

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