English
Specialized simp form of mem_uniformity_edist for basic sets.
Русский
Специализированная упрощенная форма mem_uniformity_edist для простых множеств.
LaTeX
$$$ s ∈ 𝓤 α \iff ∃ ε > 0, ∀ {a,b}, edist a b < ε \Rightarrow (a,b) ∈ s $$$
Lean4
/-- Given `f : β → ℝ≥0∞`, 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_edist`, `uniformity_basis_edist'`,
`uniformity_basis_edist_nnreal`, and `uniformity_basis_edist_inv_nat`. -/
protected theorem mk_uniformity_basis {β : 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 hf ε ε₀ with ⟨i, hi, H⟩
exact ⟨i, hi, fun x hx => hε <| lt_of_lt_of_le hx.out H⟩
· exact fun ⟨i, hi, H⟩ => ⟨f i, hf₀ i hi, H⟩
