English
Given a family of predicates p on β and a function f: β → ℝ, if f(i) > 0 whenever p(i) holds and for every ε > 0 there exists i with p(i) and f(i) ≤ ε, then the sets { (a,b) ∈ α×α | dist(a,b) < f(i) } (for i with p(i)) form a basis of the uniformity of α.
Русский
Пусть есть семейство предикатов p на β и функция f: β → ℝ. Если для каждого i с p(i) выполняется f(i) > 0, и для каждого ε > 0 существует i с p(i) и f(i) ≤ ε, то множества { (a,b) ∈ α×α | dist(a,b) < f(i) } (с такими i) образуют базис униформности α.
LaTeX
$$$$ (\mathcal{U}(\alpha)) \HasBasis p \bigl( i \mapsto \{ (a,b) \in \alpha \times \alpha \mid \operatorname{dist}(a,b) < f(i) \} \bigr) $$$$
Lean4
/-- Given `f : β → ℝ`, if `f` sends `{i | p i}` to a set of positive numbers
accumulating to zero, then `f i`-neighborhoods of the diagonal form a basis of `𝓤 α`.
For specific bases see `uniformity_basis_dist`, `uniformity_basis_dist_inv_nat_succ`,
and `uniformity_basis_dist_inv_nat_pos`. -/
protected theorem mk_uniformity_basis {β : Type*} {p : β → Prop} {f : β → ℝ} (hf₀ : ∀ i, p i → 0 < f i)
(hf : ∀ ⦃ε⦄, 0 < ε → ∃ i, p i ∧ f i ≤ ε) : (𝓤 α).HasBasis p fun i => {p : α × α | dist p.1 p.2 < f i} :=
by
refine ⟨fun s => uniformity_basis_dist.mem_iff.trans ?_⟩
constructor
· rintro ⟨ε, ε₀, hε⟩
rcases hf ε₀ with ⟨i, hi, H⟩
exact ⟨i, hi, fun x (hx : _ < _) => hε <| lt_of_lt_of_le hx H⟩
· exact fun ⟨i, hi, H⟩ => ⟨f i, hf₀ i hi, H⟩
