English
There is a basis of the uniformity given by left-continuous ≤ relation with edist bound ≤ ε.
Русский
Базис равномерности задаётся через edist с неравенством ≤ ε.
LaTeX
$$$ (𝓤 α).HasBasis (fun p => p) (fun ε => \{p : α × α | edist p.1 p.2 ≤ ε\}) $$$
Lean4
/-- Given `f : β → ℝ≥0∞`, if `f` sends `{i | p i}` to a set of positive numbers
accumulating to zero, then closed `f i`-neighborhoods of the diagonal form a basis of `𝓤 α`.
For specific bases see `uniformity_basis_edist_le` and `uniformity_basis_edist_le'`. -/
protected theorem mk_uniformity_basis_le {β : Type*} {p : β → Prop} {f : β → ℝ≥0∞} (hf₀ : ∀ x, p x → 0 < f x)
(hf : ∀ ε, 0 < ε → ∃ x, p x ∧ f x ≤ ε) : (𝓤 α).HasBasis p fun x => {p : α × α | edist p.1 p.2 ≤ f x} :=
by
refine ⟨fun s => uniformity_basis_edist.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.out H) hε'.2⟩
· exact fun ⟨i, hi, H⟩ => ⟨f i, hf₀ i hi, fun x hx => H (le_of_lt hx.out)⟩
