chore(*): fixup docs that don't parse/cause linting errors (#7088)

A couple docs had errors in the way that they were written, leading to them not displaying properly, or causing linting errors. This aims to make the [style_exceptions.txt](https://github.com/leanprover-community/mathlib/blob/master/scripts/style-exceptions.txt) file smaller, and also make the webdocs display them properly, c.f. [here](https://leanprover-community.github.io/mathlib_docs/topology/metric_space/basic.html).
leanprover-community · Apr 8, 2021 · 99c7d22 · 99c7d22
1 parent c356c1f
commit 99c7d22
Show file tree

Hide file tree

Showing 16 changed files with 93 additions and 55 deletions.
diff --git a/src/data/erased.lean b/src/data/erased.lean
@@ -5,8 +5,6 @@ Authors: Mario Carneiro
 -/
 import data.equiv.basic
 
-universes u
-
 /-!
 # A type for VM-erased data
 
@@ -15,6 +13,8 @@ but erased in the VM. That is, at runtime every value of `erased α` is
 represented as `0`, just like types and proofs.
 -/
 
+universes u
+
 /-- `erased α` is the same as `α`, except that the elements
   of `erased α` are erased in the VM in the same way as types
   and proofs. This can be used to track data without storing it

diff --git a/src/data/list/palindrome.lean b/src/data/list/palindrome.lean
@@ -5,7 +5,6 @@ Authors: Chris Wong
 -/
 
 import data.list.basic
-open list
 
 /-!
 # Palindromes
@@ -26,6 +25,8 @@ principle. Also provided are conversions to and from other equivalent definition
 palindrome, reverse, induction
 -/
 
+open list
+
 variables {α : Type*}
 
 /--

diff --git a/src/data/matrix/pequiv.lean b/src/data/matrix/pequiv.lean
@@ -5,7 +5,8 @@ Authors: Chris Hughes
 -/
 import data.matrix.basic
 import data.pequiv
-/-
+
+/-!
 # partial equivalences for matrices
 
 Using partial equivalences to represent matrices.

diff --git a/src/data/nat/modeq.lean b/src/data/nat/modeq.lean
@@ -6,7 +6,8 @@ Authors: Mario Carneiro
 import data.int.gcd
 import tactic.abel
 import data.list.rotate
-/-
+
+/-!
 # Congruences modulo a natural number
 
 This file defines the equivalence relation `a ≡ b [MOD n]` on the natural numbers,
@@ -21,6 +22,7 @@ and proves basic properties about it such as the Chinese Remainder Theorem
 
 modeq, congruence, mod, MOD, modulo
 -/
+
 namespace nat
 
 /-- Modular equality. `modeq n a b`, or `a ≡ b [MOD n]`, means

diff --git a/src/data/qpf/multivariate/basic.lean b/src/data/qpf/multivariate/basic.lean
@@ -4,7 +4,6 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Jeremy Avigad, Simon Hudon
 -/
 import data.pfunctor.multivariate.basic
-universe u
 
 /-!
 # Multivariate quotients of polynomial functors.
@@ -74,6 +73,8 @@ each proves that some operations on functors preserves the QPF structure
  * [Jeremy Avigad, Mario M. Carneiro and Simon Hudon, *Data Types as Quotients of Polynomial Functors*][avigad-carneiro-hudon2019]
 -/
 
+universe u
+
 open_locale mvfunctor
 
 /--

diff --git a/src/data/qpf/multivariate/constructions/fix.lean b/src/data/qpf/multivariate/constructions/fix.lean
@@ -5,7 +5,6 @@ Authors: Jeremy Avigad, Simon Hudon
 -/
 import data.pfunctor.multivariate.W
 import data.qpf.multivariate.basic
-universes u v
 
 /-!
 # The initial algebra of a multivariate qpf is again a qpf.
@@ -48,6 +47,8 @@ See [avigad-carneiro-hudon2019] for more details.
  * [Jeremy Avigad, Mario M. Carneiro and Simon Hudon, *Data Types as Quotients of Polynomial Functors*][avigad-carneiro-hudon2019]
 -/
 
+universes u v
+
 namespace mvqpf
 open typevec
 open mvfunctor (liftp liftr)

diff --git a/src/data/sym2.lean b/src/data/sym2.lean
@@ -6,9 +6,6 @@ Authors: Kyle Miller
 import tactic.linarith
 import data.sym
 
-open function
-open sym
-
 /-!
 # The symmetric square
 
@@ -40,6 +37,9 @@ term of the symmetric square.
 symmetric square, unordered pairs, symmetric powers
 -/
 
+open function
+open sym
+
 universe u
 variables {α : Type u}
 namespace sym2

diff --git a/src/geometry/euclidean/basic.lean b/src/geometry/euclidean/basic.lean
@@ -10,12 +10,6 @@ import data.matrix.notation
 import linear_algebra.affine_space.finite_dimensional
 import tactic.fin_cases
 
-noncomputable theory
-open_locale big_operators
-open_locale classical
-open_locale real
-open_locale real_inner_product_space
-
 /-!
 # Euclidean spaces
 
@@ -58,6 +52,12 @@ theorems that need it.
 
 -/
 
+noncomputable theory
+open_locale big_operators
+open_locale classical
+open_locale real
+open_locale real_inner_product_space
+
 namespace inner_product_geometry
 /-!
 ### Geometrical results on real inner product spaces

diff --git a/src/geometry/euclidean/circumcenter.lean b/src/geometry/euclidean/circumcenter.lean
@@ -7,12 +7,6 @@ import geometry.euclidean.basic
 import linear_algebra.affine_space.finite_dimensional
 import tactic.derive_fintype
 
-noncomputable theory
-open_locale big_operators
-open_locale classical
-open_locale real
-open_locale real_inner_product_space
-
 /-!
 # Circumcenter and circumradius
 
@@ -33,6 +27,12 @@ the circumcenter.
 
 -/
 
+noncomputable theory
+open_locale big_operators
+open_locale classical
+open_locale real
+open_locale real_inner_product_space
+
 namespace euclidean_geometry
 
 open inner_product_geometry

diff --git a/src/geometry/euclidean/monge_point.lean b/src/geometry/euclidean/monge_point.lean
@@ -5,12 +5,6 @@ Authors: Joseph Myers
 -/
 import geometry.euclidean.circumcenter
 
-noncomputable theory
-open_locale big_operators
-open_locale classical
-open_locale real
-open_locale real_inner_product_space
-
 /-!
 # Monge point and orthocenter
 
@@ -52,6 +46,12 @@ generalization, the Monge point of a simplex.
 
 -/
 
+noncomputable theory
+open_locale big_operators
+open_locale classical
+open_locale real
+open_locale real_inner_product_space
+
 namespace affine
 
 namespace simplex

diff --git a/src/geometry/euclidean/triangle.lean b/src/geometry/euclidean/triangle.lean
@@ -6,12 +6,6 @@ Authors: Joseph Myers
 import geometry.euclidean.basic
 import tactic.interval_cases
 
-noncomputable theory
-open_locale big_operators
-open_locale classical
-open_locale real
-open_locale real_inner_product_space
-
 /-!
 # Triangles
 
@@ -39,7 +33,14 @@ unnecessarily.
 
 -/
 
+noncomputable theory
+open_locale big_operators
+open_locale classical
+open_locale real
+open_locale real_inner_product_space
+
 namespace inner_product_geometry
+
 /-!
 ### Geometrical results on triangles in real inner product spaces
 

diff --git a/src/order/basic.lean b/src/order/basic.lean
@@ -6,8 +6,6 @@ Authors: Jeremy Avigad, Mario Carneiro
 import data.subtype
 import data.prod
 
-open function
-
 /-!
 # Basic definitions about `≤` and `<`
 
@@ -53,6 +51,8 @@ open function
 preorder, order, partial order, linear order, monotone, strictly monotone
 -/
 
+open function
+
 universes u v w
 variables {α : Type u} {β : Type v} {γ : Type w} {r : α → α → Prop}
 

diff --git a/src/set_theory/game/impartial.lean b/src/set_theory/game/impartial.lean
@@ -7,8 +7,6 @@ import set_theory.game.winner
 import tactic.nth_rewrite.default
 import tactic.equiv_rw
 
-universe u
-
 /-!
 # Basic definitions about impartial (pre-)games
 
@@ -18,6 +16,8 @@ no matter what moves are played. This allows for games such as poker-nim to be c
 impartial.
 -/
 
+universe u
+
 namespace pgame
 
 local infix ` ≈ ` := equiv

diff --git a/src/topology/bases.lean b/src/topology/bases.lean
@@ -2,21 +2,25 @@
 Copyright (c) 2017 Johannes Hölzl. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Johannes Hölzl, Mario Carneiro
-
-Bases of topologies. Countability axioms.
 -/
+
 import topology.continuous_on
 
+/-!
+# Bases of topologies. Countability axioms.
+
+## Implementation Notes
+For our applications we are interested that there exists a countable basis, but we do not need the
+concrete basis itself. This allows us to declare these type classes as `Prop` to use them as mixins.
+
+-/
+
 open set filter classical
 open_locale topological_space filter
 noncomputable theory
 
 namespace topological_space
-/- countability axioms
 
-For our applications we are interested that there exists a countable basis, but we do not need the
-concrete basis itself. This allows us to declare these type classes as `Prop` to use them as mixins.
--/
 universe u
 variables {α : Type u} [t : topological_space α]
 include t

diff --git a/src/topology/basic.lean b/src/topology/basic.lean
@@ -7,8 +7,6 @@ import order.filter.ultrafilter
 import order.filter.partial
 import data.support
 
-noncomputable theory
-
 /-!
 # Basic theory of topological spaces.
 
@@ -47,6 +45,7 @@ Topology in mathlib heavily uses filters (even more than in Bourbaki). See expla
 topological space, interior, closure, frontier, neighborhood, continuity, continuous function
 -/
 
+noncomputable theory
 open set filter classical
 open_locale classical filter
 

diff --git a/src/topology/metric_space/basic.lean b/src/topology/metric_space/basic.lean
@@ -1,23 +1,51 @@
 /-
 Copyright (c) 2015, 2017 Jeremy Avigad. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
-Metric spaces.
-
 Authors: Jeremy Avigad, Robert Y. Lewis, Johannes Hölzl, Mario Carneiro, Sébastien Gouëzel
+-/
+
+import topology.metric_space.emetric_space
+import topology.shrinking_lemma
+import topology.algebra.ordered
+import data.fintype.intervals
+
+/-!
+# Metric spaces
+
+This file defines metric spaces. Many definitions and theorems expected
+on metric spaces are already introduced on uniform spaces and topological spaces.
+For example: open and closed sets, compactness, completeness, continuity and uniform continuity
+
+## Main definitions
 
-Many definitions and theorems expected on metric spaces are already introduced on uniform spaces and
-topological spaces. For example:
-  open and closed sets, compactness, completeness, continuity and uniform continuity
+* `has_dist α`: Endows a space `α` with a function `dist a b`.
+* `pseudo_metric_space α`: A space endowed with a distance function, which can
+  be zero even if the two elements are non-equal.
+* `metric.ball x ε`: The set of all points `y` with `dist y x < ε`.
+* `metric.bounded s`: Whether a subset of a `pseudo_metric_space` is bounded.
+* `metric_space α`: A `pseudo_metric_space` with the guarantee `dist x y = 0 → x = y`.
+
+Additional useful definitions:
+
+* `nndist a b`: `dist` as a function to the non-negative reals.
+* `metric.closed_ball x ε`: The set of all points `y` with `dist y x ≤ ε`.
+* `metric.sphere x ε`: The set of all points `y` with `dist y x = ε`.
+* `proper_space α`: A `pseudo_metric_space` where all closed balls are compact.
+* `metric.diam s` : The `supr` of the distances of members of `s`.
+  Defined in terms of `emetric.diam`, for better handling of the case when it should be infinite.
+
+TODO (anyone): Add "Main results" section.
+
+## Implementation notes
 
 Since a lot of elementary properties don't require `eq_of_dist_eq_zero` we start setting up the
 theory of `pseudo_metric_space`, where we don't require `dist x y = 0 → x = y` and we specialize
 to `metric_space` at the end.
 
+## Tags
+
+metric, pseudo_metric, dist
 -/
-import topology.metric_space.emetric_space
-import topology.shrinking_lemma
-import topology.algebra.ordered
-import data.fintype.intervals
 
 open set filter topological_space
 noncomputable theory