eventually_uniformity_comp_subset

English

Given an entourage s ∈ 𝓤 α and n ∈ ℕ, there exists a smaller t (in the smallSets of 𝓤 α) such that t ○ t ○ ... ○ t ⊆ s (n times).

Русский

Для каждого окружения s ∈ 𝓤 α и натурального n существует меньшая t (из smallSets) такая, что t ○ t ○ ... ○ t ⊆ s (n раз).

LaTeX

$$$\\forall n, \\exists t \\in (\\mathcal{U}\\alpha).smallSets, (t ○ ·)^{[n]} t \\subseteq s$$$

Lean4

/-- If `s ∈ 𝓤 α`, then for a subset `t` of a sufficiently small set in `𝓤 α`,
we have `t ○ t ⊆ s`. -/
theorem eventually_uniformity_comp_subset {s : Set (α × α)} (hs : s ∈ 𝓤 α) : ∀ᶠ t in (𝓤 α).smallSets, t ○ t ⊆ s :=
  eventually_uniformity_iterate_comp_subset hs 1

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