Skip to content

Commit

Permalink
fix: remove no-break spaces in Topology.UniformSpace.Basic (#6560)
Browse files Browse the repository at this point in the history
This caused titles to not show properly in docs.
  • Loading branch information
ADedecker committed Aug 15, 2023
1 parent 280a9f5 commit 63cf080
Showing 1 changed file with 2 additions and 2 deletions.
4 changes: 2 additions & 2 deletions Mathlib/Topology/UniformSpace/Basic.lean
Expand Up @@ -74,7 +74,7 @@ The uniform space axioms ask the filter `𝓤 X` to satisfy the following:
These three axioms are stated more abstractly in the definition below, in terms of
operations on filters, without directly manipulating entourages.
## Main definitions
## Main definitions
* `UniformSpace X` is a uniform space structure on a type `X`
* `UniformContinuous f` is a predicate saying a function `f : α → β` between uniform spaces
Expand Down Expand Up @@ -607,7 +607,7 @@ theorem comp_comp_symm_mem_uniformity_sets {s : Set (α × α)} (hs : s ∈ 𝓤
#align comp_comp_symm_mem_uniformity_sets comp_comp_symm_mem_uniformity_sets

/-!
### Balls in uniform spaces
### Balls in uniform spaces
-/

/-- The ball around `(x : β)` with respect to `(V : Set (β × β))`. Intended to be
Expand Down

0 comments on commit 63cf080

Please sign in to comment.