doc: add docstrings for ChartedSpace.{atlas,chartAt} and their aliases (

#10169)

Mathlib/Geometry/Manifold/ChartedSpace.lean

@@ -555,16 +555,20 @@ sometimes as a real manifold over `ℝ^(2n)`.
 -/
 @[ext]
 class ChartedSpace (H : Type*) [TopologicalSpace H] (M : Type*) [TopologicalSpace M] where
+  /-- The atlas of charts in the `ChartedSpace`. -/
   protected atlas : Set (PartialHomeomorph M H)
+  /-- The preferred chart at each point in the charted space. -/
   protected chartAt : M → PartialHomeomorph M H
   protected mem_chart_source : ∀ x, x ∈ (chartAt x).source
   protected chart_mem_atlas : ∀ x, chartAt x ∈ atlas
 #align charted_space ChartedSpace
 
+/-- The atlas of charts in a `ChartedSpace`. -/
 abbrev atlas (H : Type*) [TopologicalSpace H] (M : Type*) [TopologicalSpace M]
     [ChartedSpace H M] : Set (PartialHomeomorph M H) :=
   ChartedSpace.atlas
 
+/-- The preferred chart at a point `x` in a charted space `M`. -/
 abbrev chartAt (H : Type*) [TopologicalSpace H] {M : Type*} [TopologicalSpace M]
     [ChartedSpace H M] (x : M) : PartialHomeomorph M H :=
   ChartedSpace.chartAt x

scripts/nolints.json

@@ -43,13 +43,11 @@
  ["docBlame", "WriterT"],
  ["docBlame", "Xor'"],
  ["docBlame", "Zero"],
- ["docBlame", "atlas"],
  ["docBlame", "bit0"],
  ["docBlame", "bit1"],
  ["docBlame", "cancelDenominators"],
  ["docBlame", "cancelDenominatorsAt"],
  ["docBlame", "cancelDenominatorsTarget"],
- ["docBlame", "chartAt"],
  ["docBlame", "condM"],
  ["docBlame", "decidableEq_of_bool_pred"],
  ["docBlame", "eqns"],
@@ -121,8 +119,6 @@
  ["docBlame", "Cardinal.term𝔠"],
  ["docBlame", "CategoryTheory.«term_⟶[_]_»"],
  ["docBlame", "ChangeOfRings.«term_⊗ₜ[_,_]_»"],
- ["docBlame", "ChartedSpace.atlas"],
- ["docBlame", "ChartedSpace.chartAt"],
  ["docBlame", "ChartedSpaceCore.atlas"],
  ["docBlame", "ChartedSpaceCore.chartAt"],
  ["docBlame", "Combinator.I"],