Module docstring
{"# Construct a UniformSpace from a dist-like function
In this file we provide a constructor for UniformSpace
given a dist-like function
TODO
RFC: use UniformSpace.Core.mkOfBasis? This will change defeq here and there
"}
UniformSpace.ofFun
definition
[AddCommMonoid M] [PartialOrder M] (d : X → X → M) (refl : ∀ x, d x x = 0) (symm : ∀ x y, d x y = d y x)
(triangle : ∀ x y z, d x z ≤ d x y + d y z) (half : ∀ ε > (0 : M), ∃ δ > (0 : M), ∀ x < δ, ∀ y < δ, x + y < ε) :
UniformSpace X
Full source
/-- Define a `UniformSpace` using a "distance" function. The function can be, e.g., the
distance in a (usual or extended) metric space or an absolute value on a ring. -/
def ofFun [AddCommMonoid M] [PartialOrder M]
(d : X → X → M) (refl : ∀ x, d x x = 0)
(symm : ∀ x y, d x y = d y x) (triangle : ∀ x y z, d x z ≤ d x y + d y z)
(half : ∀ ε > (0 : M), ∃ δ > (0 : M), ∀ x < δ, ∀ y < δ, x + y < ε) :
UniformSpace X :=
.ofCore
{ uniformity := ⨅ r > 0, 𝓟 { x | d x.1 x.2 < r }
refl := le_iInf₂ fun r hr => principal_mono.2 <| idRel_subset.2 fun x => by simpa [refl]
symm := tendsto_iInf_iInf fun r => tendsto_iInf_iInf fun _ => tendsto_principal_principal.2
fun x hx => by rwa [mem_setOf, symm]
comp := le_iInf₂ fun r hr => let ⟨δ, h0, hδr⟩ := half r hr; le_principal_iff.2 <|
mem_of_superset
(mem_lift' <| mem_iInf_of_mem δ <| mem_iInf_of_mem h0 <| mem_principal_self _)
fun (x, z) ⟨y, h₁, h₂⟩ => (triangle _ _ _).trans_lt (hδr _ h₁ _ h₂) }Informal description
Given a type $X$ and an additive commutative monoid $M$ with a partial order, a function $d : X \times X \to M$ defines a uniform space structure on $X$ if it satisfies the following properties:
1. **Reflexivity**: $d(x, x) = 0$ for all $x \in X$.
2. **Symmetry**: $d(x, y) = d(y, x)$ for all $x, y \in X$.
3. **Triangle inequality**: $d(x, z) \leq d(x, y) + d(y, z)$ for all $x, y, z \in X$.
4. **Approximation property**: For every $\varepsilon > 0$ in $M$, there exists $\delta > 0$ such that for all $x, y \in M$, if $x < \delta$ and $y < \delta$, then $x + y < \varepsilon$.
The uniformity filter is generated by the sets $\{(x, y) \mid d(x, y) < r\}$ for $r > 0$.
UniformSpace.hasBasis_ofFun
theorem
[AddCommMonoid M] [LinearOrder M] (h₀ : ∃ x : M, 0 < x) (d : X → X → M) (refl : ∀ x, d x x = 0)
(symm : ∀ x y, d x y = d y x) (triangle : ∀ x y z, d x z ≤ d x y + d y z)
(half : ∀ ε > (0 : M), ∃ δ > (0 : M), ∀ x < δ, ∀ y < δ, x + y < ε) :
𝓤[.ofFun d refl symm triangle half].HasBasis ((0 : M) < ·) (fun ε => {x | d x.1 x.2 < ε})
Full source
theorem hasBasis_ofFun [AddCommMonoid M] [LinearOrder M]
(h₀ : ∃ x : M, 0 < x) (d : X → X → M) (refl : ∀ x, d x x = 0) (symm : ∀ x y, d x y = d y x)
(triangle : ∀ x y z, d x z ≤ d x y + d y z)
(half : ∀ ε > (0 : M), ∃ δ > (0 : M), ∀ x < δ, ∀ y < δ, x + y < ε) :
𝓤[.ofFun d refl symm triangle half].HasBasis ((0 : M) < ·) (fun ε => { x | d x.1 x.2 < ε }) :=
hasBasis_biInf_principal'
(fun ε₁ h₁ ε₂ h₂ => ⟨min ε₁ ε₂, lt_min h₁ h₂, fun _x hx => lt_of_lt_of_le hx (min_le_left _ _),
fun _x hx => lt_of_lt_of_le hx (min_le_right _ _)⟩) h₀Informal description
Let $M$ be an additively commutative monoid with a linear order, and suppose there exists an element $x \in M$ with $0 < x$. Given a function $d : X \times X \to M$ satisfying:
1. **Reflexivity**: $d(x, x) = 0$ for all $x \in X$,
2. **Symmetry**: $d(x, y) = d(y, x)$ for all $x, y \in X$,
3. **Triangle inequality**: $d(x, z) \leq d(x, y) + d(y, z)$ for all $x, y, z \in X$,
4. **Approximation property**: For every $\varepsilon > 0$ in $M$, there exists $\delta > 0$ such that for all $x, y \in M$, if $x < \delta$ and $y < \delta$, then $x + y < \varepsilon$,
then the uniformity filter $\mathfrak{U}(X)$ of the uniform space constructed from $d$ has a basis consisting of the sets $\{(x, y) \mid d(x, y) < \varepsilon\}$ for all $\varepsilon > 0$ in $M$.