English
For a real r with 0 < r < 1, the entourages { (a,b) | dist(a,b) ≤ r^n } for n ∈ ℕ form a basis of the uniformity.
Русский
Пусть 0 < r < 1. Окружности { (a,b) | dist(a,b) ≤ r^n } (n∈ℕ) образуют базис униформности.
LaTeX
$$$$ (\mathcal{U}(\alpha)) \HasBasis (n \in \mathbb{N}) \bigl( n \mapsto \{ (a,b) \in \alpha \times \alpha \mid \operatorname{dist}(a,b) \le r^{n} \} \bigr) $$$$
Lean4
/-- Given `f : β → ℝ`, if `f` sends `{i | p i}` to a set of positive numbers
accumulating to zero, then closed neighborhoods of the diagonal of sizes `{f i | p i}`
form a basis of `𝓤 α`.
Currently we have only one specific basis `uniformity_basis_dist_le` based on this constructor.
More can be easily added if needed in the future. -/
protected theorem mk_uniformity_basis_le {β : Type*} {p : β → Prop} {f : β → ℝ} (hf₀ : ∀ x, p x → 0 < f x)
(hf : ∀ ε, 0 < ε → ∃ x, p x ∧ f x ≤ ε) : (𝓤 α).HasBasis p fun x => {p : α × α | dist p.1 p.2 ≤ f x} :=
by
refine ⟨fun s => uniformity_basis_dist.mem_iff.trans ?_⟩
constructor
· rintro ⟨ε, ε₀, hε⟩
rcases exists_between ε₀ with ⟨ε', hε'⟩
rcases hf ε' hε'.1 with ⟨i, hi, H⟩
exact ⟨i, hi, fun x (hx : _ ≤ _) => hε <| lt_of_le_of_lt (le_trans hx H) hε'.2⟩
· exact fun ⟨i, hi, H⟩ => ⟨f i, hf₀ i hi, fun x (hx : _ < _) => H (mem_setOf.2 hx.le)⟩
