From 14165fc8dc7c5021590cebece34b487ba32a3548 Mon Sep 17 00:00:00 2001 From: grunweg Date: Thu, 20 Feb 2025 10:22:27 +0000 Subject: [PATCH] style(Geometry/Manifold): remove superfluous indentation in doc-strings (#22117) [Zulip discussion](https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/Style.20.3Abicycle.3A.20.3A.20indenting.20second.20lines.20in.20doc-strings) --- Mathlib/Geometry/Manifold/ChartedSpace.lean | 10 ++--- Mathlib/Geometry/Manifold/ContMDiff/Defs.lean | 18 ++++----- .../Manifold/IntegralCurve/Basic.lean | 2 +- .../Manifold/IntegralCurve/UniformTime.lean | 37 +++++++++---------- .../Geometry/Manifold/IsManifold/Basic.lean | 8 ++-- .../Manifold/IsManifold/ExtChartAt.lean | 7 ++-- .../Manifold/IsManifold/InteriorBoundary.lean | 2 +- .../Geometry/Manifold/LocalDiffeomorph.lean | 4 +- Mathlib/Geometry/Manifold/MFDeriv/Basic.lean | 18 ++++----- .../Geometry/Manifold/PartitionOfUnity.lean | 4 +- 10 files changed, 54 insertions(+), 56 deletions(-) diff --git a/Mathlib/Geometry/Manifold/ChartedSpace.lean b/Mathlib/Geometry/Manifold/ChartedSpace.lean index fa6429f19968c..6f7534a54556f 100644 --- a/Mathlib/Geometry/Manifold/ChartedSpace.lean +++ b/Mathlib/Geometry/Manifold/ChartedSpace.lean @@ -677,7 +677,7 @@ theorem ChartedSpace.locallyConnectedSpace [LocallyConnectedSpace H] : LocallyCo exact hsconn.isPreconnected.image _ ((e x).continuousOn_symm.mono hssubset) /-- If a topological space `M` admits an atlas with locally path-connected charts, - then `M` itself is locally path-connected. -/ +then `M` itself is locally path-connected. -/ theorem ChartedSpace.locPathConnectedSpace [LocPathConnectedSpace H] : LocPathConnectedSpace M := by refine ⟨fun x ↦ ⟨fun s ↦ ⟨fun hs ↦ ?_, fun ⟨u, hu⟩ ↦ Filter.mem_of_superset hu.1.1 hu.2⟩⟩⟩ let e := chartAt H x @@ -1090,8 +1090,8 @@ instance hasGroupoid_continuousGroupoid : HasGroupoid M (continuousGroupoid H) : rw [continuousGroupoid, mem_groupoid_of_pregroupoid] simp only [and_self_iff] -/-- If `G` is closed under restriction, the transition function between - the restriction of two charts `e` and `e'` lies in `G`. -/ +/-- If `G` is closed under restriction, the transition function between the restriction of two +charts `e` and `e'` lies in `G`. -/ theorem StructureGroupoid.trans_restricted {e e' : PartialHomeomorph M H} {G : StructureGroupoid H} (he : e ∈ atlas H M) (he' : e' ∈ atlas H M) [HasGroupoid M G] [ClosedUnderRestriction G] {s : Opens M} (hs : Nonempty s) : @@ -1261,14 +1261,14 @@ protected instance instChartedSpace : ChartedSpace H s where use x /-- If `s` is a non-empty open subset of `M`, every chart of `s` is the restriction - of some chart on `M`. -/ +of some chart on `M`. -/ lemma chart_eq {s : Opens M} (hs : Nonempty s) {e : PartialHomeomorph s H} (he : e ∈ atlas H s) : ∃ x : s, e = (chartAt H (x : M)).subtypeRestr hs := by rcases he with ⟨xset, ⟨x, hx⟩, he⟩ exact ⟨x, mem_singleton_iff.mp (by convert he)⟩ /-- If `t` is a non-empty open subset of `H`, - every chart of `t` is the restriction of some chart on `H`. -/ +every chart of `t` is the restriction of some chart on `H`. -/ -- XXX: can I unify this with `chart_eq`? lemma chart_eq' {t : Opens H} (ht : Nonempty t) {e' : PartialHomeomorph t H} (he' : e' ∈ atlas H t) : ∃ x : t, e' = (chartAt H ↑x).subtypeRestr ht := by diff --git a/Mathlib/Geometry/Manifold/ContMDiff/Defs.lean b/Mathlib/Geometry/Manifold/ContMDiff/Defs.lean index 8b8ece0aafb7a..53b65753c614b 100644 --- a/Mathlib/Geometry/Manifold/ContMDiff/Defs.lean +++ b/Mathlib/Geometry/Manifold/ContMDiff/Defs.lean @@ -368,7 +368,7 @@ theorem contMDiffWithinAt_iff_of_mem_maximalAtlas {x : M} (he : e ∈ maximalAtl (contDiffWithinAt_localInvariantProp n).liftPropWithinAt_indep_chart he hx he' hy /-- An alternative formulation of `contMDiffWithinAt_iff_of_mem_maximalAtlas` - if the set if `s` lies in `e.source`. -/ +if the set if `s` lies in `e.source`. -/ theorem contMDiffWithinAt_iff_image {x : M} (he : e ∈ maximalAtlas I n M) (he' : e' ∈ maximalAtlas I' n M') (hs : s ⊆ e.source) (hx : x ∈ e.source) (hy : f x ∈ e'.source) : @@ -434,10 +434,10 @@ theorem contMDiffOn_iff_of_mem_maximalAtlas' (he : e ∈ maximalAtlas I n M) (e.continuousOn_writtenInExtend_iff hs h2s).1 h.continuousOn /-- If the set where you want `f` to be `C^n` lies entirely in a single chart, and `f` maps it - into a single chart, the fact that `f` is `C^n` on that set can be expressed by purely looking in - these charts. - Note: this lemma uses `extChartAt I x '' s` instead of `(extChartAt I x).symm ⁻¹' s` to ensure - that this set lies in `(extChartAt I x).target`. -/ +into a single chart, the fact that `f` is `C^n` on that set can be expressed by purely looking in +these charts. +Note: this lemma uses `extChartAt I x '' s` instead of `(extChartAt I x).symm ⁻¹' s` to ensure +that this set lies in `(extChartAt I x).target`. -/ theorem contMDiffOn_iff_of_subset_source {x : M} {y : M'} (hs : s ⊆ (chartAt H x).source) (h2s : MapsTo f s (chartAt H' y).source) : ContMDiffOn I I' n f s ↔ @@ -447,10 +447,10 @@ theorem contMDiffOn_iff_of_subset_source {x : M} {y : M'} (hs : s ⊆ (chartAt H h2s /-- If the set where you want `f` to be `C^n` lies entirely in a single chart, and `f` maps it - into a single chart, the fact that `f` is `C^n` on that set can be expressed by purely looking in - these charts. - Note: this lemma uses `extChartAt I x '' s` instead of `(extChartAt I x).symm ⁻¹' s` to ensure - that this set lies in `(extChartAt I x).target`. -/ +into a single chart, the fact that `f` is `C^n` on that set can be expressed by purely looking in +these charts. +Note: this lemma uses `extChartAt I x '' s` instead of `(extChartAt I x).symm ⁻¹' s` to ensure +that this set lies in `(extChartAt I x).target`. -/ theorem contMDiffOn_iff_of_subset_source' {x : M} {y : M'} (hs : s ⊆ (extChartAt I x).source) (h2s : MapsTo f s (extChartAt I' y).source) : ContMDiffOn I I' n f s ↔ diff --git a/Mathlib/Geometry/Manifold/IntegralCurve/Basic.lean b/Mathlib/Geometry/Manifold/IntegralCurve/Basic.lean index ded16e66a8c2c..74bfc3d721dfb 100644 --- a/Mathlib/Geometry/Manifold/IntegralCurve/Basic.lean +++ b/Mathlib/Geometry/Manifold/IntegralCurve/Basic.lean @@ -137,7 +137,7 @@ lemma IsIntegralCurve.continuous (hγ : IsIntegralCurve γ v) : Continuous γ := variable [IsManifold I 1 M] /-- If `γ` is an integral curve of a vector field `v`, then `γ t` is tangent to `v (γ t)` when - expressed in the local chart around the initial point `γ t₀`. -/ +expressed in the local chart around the initial point `γ t₀`. -/ lemma IsIntegralCurveOn.hasDerivAt (hγ : IsIntegralCurveOn γ v s) {t : ℝ} (ht : t ∈ s) (hsrc : γ t ∈ (extChartAt I (γ t₀)).source) : HasDerivAt ((extChartAt I (γ t₀)) ∘ γ) diff --git a/Mathlib/Geometry/Manifold/IntegralCurve/UniformTime.lean b/Mathlib/Geometry/Manifold/IntegralCurve/UniformTime.lean index dc59d2f38f78e..c88c33088860c 100644 --- a/Mathlib/Geometry/Manifold/IntegralCurve/UniformTime.lean +++ b/Mathlib/Geometry/Manifold/IntegralCurve/UniformTime.lean @@ -34,7 +34,7 @@ variable [T2Space M] {γ γ' : ℝ → M} {v : (x : M) → TangentSpace I x} {s s' : Set ℝ} {t₀ : ℝ} /-- This is the uniqueness theorem of integral curves applied to a real-indexed family of integral - curves with the same starting point. -/ +curves with the same starting point. -/ lemma eqOn_of_isIntegralCurveOn_Ioo [BoundarylessManifold I M] (hv : ContMDiff I I.tangent 1 (fun x ↦ (⟨x, v x⟩ : TangentBundle I M))) {x : M} (γ : ℝ → ℝ → M) (hγx : ∀ a, γ a 0 = x) (hγ : ∀ a > 0, IsIntegralCurveOn (γ a) v (Ioo (-a) a)) @@ -48,9 +48,8 @@ lemma eqOn_of_isIntegralCurveOn_Ioo [BoundarylessManifold I M] · apply Ioo_subset_Ioo <;> linarith /-- For a family of integral curves `γ : ℝ → ℝ → M` with the same starting point `γ 0 = x` such that - each `γ a` is defined on `Ioo (-a) a`, the global curve `γ_ext := fun t ↦ γ (|t| + 1) t` agrees - with each `γ a` on `Ioo (-a) a`. This will help us show that `γ_ext` is a global integral - curve. -/ +each `γ a` is defined on `Ioo (-a) a`, the global curve `γ_ext := fun t ↦ γ (|t| + 1) t` agrees +with each `γ a` on `Ioo (-a) a`. This will help us show that `γ_ext` is a global integral curve. -/ lemma eqOn_abs_add_one_of_isIntegralCurveOn_Ioo [BoundarylessManifold I M] (hv : ContMDiff I I.tangent 1 (fun x ↦ (⟨x, v x⟩ : TangentBundle I M))) {x : M} (γ : ℝ → ℝ → M) (hγx : ∀ a, γ a 0 = x) (hγ : ∀ a > 0, IsIntegralCurveOn (γ a) v (Ioo (-a) a)) @@ -63,8 +62,8 @@ lemma eqOn_abs_add_one_of_isIntegralCurveOn_Ioo [BoundarylessManifold I M] (neg_lt_self_iff.mp <| lt_trans ht.1 ht.2) (not_lt.mp hlt) ht |>.symm /-- For a family of integral curves `γ : ℝ → ℝ → M` with the same starting point `γ 0 = x` such that - each `γ a` is defined on `Ioo (-a) a`, the function `γ_ext := fun t ↦ γ (|t| + 1) t` is a global - integral curve. -/ +each `γ a` is defined on `Ioo (-a) a`, the function `γ_ext := fun t ↦ γ (|t| + 1) t` is a global +integral curve. -/ lemma isIntegralCurve_abs_add_one_of_isIntegralCurveOn_Ioo [BoundarylessManifold I M] (hv : ContMDiff I I.tangent 1 (fun x ↦ (⟨x, v x⟩ : TangentBundle I M))) {x : M} (γ : ℝ → ℝ → M) (hγx : ∀ a, γ a 0 = x) (hγ : ∀ a > 0, IsIntegralCurveOn (γ a) v (Ioo (-a) a)) : @@ -82,8 +81,8 @@ lemma isIntegralCurve_abs_add_one_of_isIntegralCurveOn_Ioo [BoundarylessManifold exact Ioo_mem_nhds this.1 this.2 /-- The existence of a global integral curve is equivalent to the existence of a family of local - integral curves `γ : ℝ → ℝ → M` with the same starting point `γ 0 = x` such that each `γ a` is - defined on `Ioo (-a) a`. -/ +integral curves `γ : ℝ → ℝ → M` with the same starting point `γ 0 = x` such that each `γ a` is +defined on `Ioo (-a) a`. -/ lemma exists_isIntegralCurve_iff_exists_isIntegralCurveOn_Ioo [BoundarylessManifold I M] (hv : ContMDiff I I.tangent 1 (fun x ↦ (⟨x, v x⟩ : TangentBundle I M))) (x : M) : (∃ γ, γ 0 = x ∧ IsIntegralCurve γ v) ↔ @@ -94,9 +93,9 @@ lemma exists_isIntegralCurve_iff_exists_isIntegralCurveOn_Ioo [BoundarylessManif isIntegralCurve_abs_add_one_of_isIntegralCurveOn_Ioo hv γ hγx (fun a _ ↦ hγ a)⟩ /-- Let `γ` and `γ'` be integral curves defined on `Ioo a b` and `Ioo a' b'`, respectively. Then, - `piecewise (Ioo a b) γ γ'` is equal to `γ` and `γ'` in their respective domains. - `Set.piecewise_eqOn` shows the equality for `γ` by definition, while this lemma shows the equality - for `γ'` by the uniqueness of integral curves. -/ +`piecewise (Ioo a b) γ γ'` is equal to `γ` and `γ'` in their respective domains. +`Set.piecewise_eqOn` shows the equality for `γ` by definition, while this lemma shows the equality +for `γ'` by the uniqueness of integral curves. -/ lemma eqOn_piecewise_of_isIntegralCurveOn_Ioo [BoundarylessManifold I M] (hv : ContMDiff I I.tangent 1 (fun x ↦ (⟨x, v x⟩ : TangentBundle I M))) {a b a' b' : ℝ} (hγ : IsIntegralCurveOn γ v (Ioo a b)) @@ -117,12 +116,12 @@ lemma eqOn_piecewise_of_isIntegralCurveOn_Ioo [BoundarylessManifold I M] /-- The extension of an integral curve by another integral curve is an integral curve. - If two integral curves are defined on overlapping open intervals, and they agree at a point in - their common domain, then they can be patched together to form a longer integral curve. +If two integral curves are defined on overlapping open intervals, and they agree at a point in +their common domain, then they can be patched together to form a longer integral curve. - This is stated for manifolds without boundary for simplicity. We actually only need to assume that - the images of `γ` and `γ'` lie in the interior of the manifold. TODO: Generalise to manifolds with - boundary. -/ +This is stated for manifolds without boundary for simplicity. We actually only need to assume that +the images of `γ` and `γ'` lie in the interior of the manifold. +TODO: Generalise to manifolds with boundary. -/ lemma isIntegralCurveOn_piecewise [BoundarylessManifold I M] (hv : ContMDiff I I.tangent 1 (fun x ↦ (⟨x, v x⟩ : TangentBundle I M))) {a b a' b' : ℝ} (hγ : IsIntegralCurveOn γ v (Ioo a b)) @@ -145,10 +144,10 @@ lemma isIntegralCurveOn_piecewise [BoundarylessManifold I M] eqOn_piecewise_of_isIntegralCurveOn_Ioo hv hγ hγ' ht₀ h⟩ /-- If there exists `ε > 0` such that the local integral curve at each point `x : M` is defined at - least on an open interval `Ioo (-ε) ε`, then every point on `M` has a global integral - curve passing through it. +least on an open interval `Ioo (-ε) ε`, then every point on `M` has a global integral curve +passing through it. - See Lemma 9.15, [J.M. Lee (2012)][lee2012]. -/ +See Lemma 9.15, [J.M. Lee (2012)][lee2012]. -/ lemma exists_isIntegralCurve_of_isIntegralCurveOn [BoundarylessManifold I M] {v : (x : M) → TangentSpace I x} (hv : ContMDiff I I.tangent 1 (fun x ↦ (⟨x, v x⟩ : TangentBundle I M))) diff --git a/Mathlib/Geometry/Manifold/IsManifold/Basic.lean b/Mathlib/Geometry/Manifold/IsManifold/Basic.lean index 41ed0d79f0ef6..b71e064332c9f 100644 --- a/Mathlib/Geometry/Manifold/IsManifold/Basic.lean +++ b/Mathlib/Geometry/Manifold/IsManifold/Basic.lean @@ -194,7 +194,7 @@ protected def symm : PartialEquiv E H := I.toPartialEquiv.symm /-- See Note [custom simps projection]. We need to specify this projection explicitly in this case, - because it is a composition of multiple projections. -/ +because it is a composition of multiple projections. -/ def Simps.apply (𝕜 : Type*) [NontriviallyNormedField 𝕜] (E : Type*) [NormedAddCommGroup E] [NormedSpace 𝕜 E] (H : Type*) [TopologicalSpace H] (I : ModelWithCorners 𝕜 E H) : H → E := I @@ -480,8 +480,8 @@ end ModelWithCornersProd section Boundaryless /-- Property ensuring that the model with corners `I` defines manifolds without boundary. This - differs from the more general `BoundarylessManifold`, which requires every point on the manifold - to be an interior point. -/ +differs from the more general `BoundarylessManifold`, which requires every point on the manifold +to be an interior point. -/ class ModelWithCorners.Boundaryless {𝕜 : Type*} [NontriviallyNormedField 𝕜] {E : Type*} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type*} [TopologicalSpace H] (I : ModelWithCorners 𝕜 E H) : Prop where @@ -569,7 +569,7 @@ def contDiffPregroupoid : Pregroupoid H where variable (n I) in /-- Given a model with corners `(E, H)`, we define the groupoid of invertible `C^n` transformations - of `H` as the invertible maps that are `C^n` when read in `E` through `I`. -/ +of `H` as the invertible maps that are `C^n` when read in `E` through `I`. -/ def contDiffGroupoid : StructureGroupoid H := Pregroupoid.groupoid (contDiffPregroupoid n I) diff --git a/Mathlib/Geometry/Manifold/IsManifold/ExtChartAt.lean b/Mathlib/Geometry/Manifold/IsManifold/ExtChartAt.lean index 86d84019af599..1e153b3acbcdb 100644 --- a/Mathlib/Geometry/Manifold/IsManifold/ExtChartAt.lean +++ b/Mathlib/Geometry/Manifold/IsManifold/ExtChartAt.lean @@ -154,7 +154,7 @@ lemma interior_extend_target_subset_interior_range : exact inter_subset_right /-- If `y ∈ f.target` and `I y ∈ interior (range I)`, - then `I y` is an interior point of `(I ∘ f).target`. -/ +then `I y` is an interior point of `(I ∘ f).target`. -/ lemma mem_interior_extend_target {y : H} (hy : y ∈ f.target) (hy' : I y ∈ interior (range I)) : I y ∈ interior (f.extend I).target := by rw [f.extend_target, interior_inter, (f.open_target.preimage I.continuous_symm).interior_eq, @@ -781,7 +781,7 @@ variable {M : Type*} [TopologicalSpace M] [ChartedSpace H M] /-- A finite-dimensional manifold modelled on a locally compact field - (such as ℝ, ℂ or the `p`-adic numbers) is locally compact. -/ +(such as ℝ, ℂ or the `p`-adic numbers) is locally compact. -/ lemma Manifold.locallyCompact_of_finiteDimensional (I : ModelWithCorners 𝕜 E H) [LocallyCompactSpace 𝕜] [FiniteDimensional 𝕜 E] : LocallyCompactSpace M := by @@ -811,8 +811,7 @@ lemma LocallyCompactSpace.of_locallyCompact_manifold (I : ModelWithCorners 𝕜 exact interior_mono (extChartAt_target_subset_range x) hy /-- Riesz's theorem applied to manifolds: a locally compact manifolds must be modelled on a - finite-dimensional space. This is the converse to - `Manifold.locallyCompact_of_finiteDimensional`. -/ +finite-dimensional space. This is the converse to `Manifold.locallyCompact_of_finiteDimensional`. -/ theorem FiniteDimensional.of_locallyCompact_manifold [CompleteSpace 𝕜] (I : ModelWithCorners 𝕜 E H) [Nonempty M] [LocallyCompactSpace M] : FiniteDimensional 𝕜 E := by diff --git a/Mathlib/Geometry/Manifold/IsManifold/InteriorBoundary.lean b/Mathlib/Geometry/Manifold/IsManifold/InteriorBoundary.lean index de97c58a28801..cb92a0c6222fd 100644 --- a/Mathlib/Geometry/Manifold/IsManifold/InteriorBoundary.lean +++ b/Mathlib/Geometry/Manifold/IsManifold/InteriorBoundary.lean @@ -131,7 +131,7 @@ lemma _root_.range_mem_nhds_isInteriorPoint {x : M} (h : I.IsInteriorPoint x) : exact ⟨interior (range I), interior_subset, isOpen_interior, h⟩ /-- Type class for manifold without boundary. This differs from `ModelWithCorners.Boundaryless`, - which states that the `ModelWithCorners` maps to the whole model vector space. -/ +which states that the `ModelWithCorners` maps to the whole model vector space. -/ class _root_.BoundarylessManifold {𝕜 : Type*} [NontriviallyNormedField 𝕜] {E : Type*} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type*} [TopologicalSpace H] (I : ModelWithCorners 𝕜 E H) diff --git a/Mathlib/Geometry/Manifold/LocalDiffeomorph.lean b/Mathlib/Geometry/Manifold/LocalDiffeomorph.lean index 19fdac1d55a45..020672e4c28c6 100644 --- a/Mathlib/Geometry/Manifold/LocalDiffeomorph.lean +++ b/Mathlib/Geometry/Manifold/LocalDiffeomorph.lean @@ -133,12 +133,12 @@ end PartialDiffeomorph variable {M N} /-- `f : M → N` is called a **`C^n` local diffeomorphism at *x*** iff there exist - open sets `U ∋ x` and `V ∋ f x` and a diffeomorphism `Φ : U → V` such that `f = Φ` on `U`. -/ +open sets `U ∋ x` and `V ∋ f x` and a diffeomorphism `Φ : U → V` such that `f = Φ` on `U`. -/ def IsLocalDiffeomorphAt (f : M → N) (x : M) : Prop := ∃ Φ : PartialDiffeomorph I J M N n, x ∈ Φ.source ∧ EqOn f Φ Φ.source /-- `f : M → N` is called a **`C^n` local diffeomorphism on *s*** iff it is a local diffeomorphism - at each `x : s`. -/ +at each `x : s`. -/ def IsLocalDiffeomorphOn (f : M → N) (s : Set M) : Prop := ∀ x : s, IsLocalDiffeomorphAt I J n f x diff --git a/Mathlib/Geometry/Manifold/MFDeriv/Basic.lean b/Mathlib/Geometry/Manifold/MFDeriv/Basic.lean index 6bd40ebe778e9..4e98602cb10b7 100644 --- a/Mathlib/Geometry/Manifold/MFDeriv/Basic.lean +++ b/Mathlib/Geometry/Manifold/MFDeriv/Basic.lean @@ -296,7 +296,7 @@ theorem mdifferentiableWithinAt_iff_of_mem_maximalAtlas {x : M} (he : e ∈ maxi differentiableWithinAt_localInvariantProp.liftPropWithinAt_indep_chart he hx he' hy /-- An alternative formulation of `mdifferentiableWithinAt_iff_of_mem_maximalAtlas` - if the set if `s` lies in `e.source`. -/ +if the set if `s` lies in `e.source`. -/ theorem mdifferentiableWithinAt_iff_image {x : M} (he : e ∈ maximalAtlas I 1 M) (he' : e' ∈ maximalAtlas I' 1 M') (hs : s ⊆ e.source) (hx : x ∈ e.source) (hy : f x ∈ e'.source) : @@ -365,10 +365,10 @@ theorem mdifferentiableOn_iff_of_mem_maximalAtlas' (he : e ∈ maximalAtlas I 1 (e.continuousOn_writtenInExtend_iff hs h2s).1 h.continuousOn /-- If the set where you want `f` to be smooth lies entirely in a single chart, and `f` maps it - into a single chart, the smoothness of `f` on that set can be expressed by purely looking in - these charts. - Note: this lemma uses `extChartAt I x '' s` instead of `(extChartAt I x).symm ⁻¹' s` to ensure - that this set lies in `(extChartAt I x).target`. -/ +into a single chart, the smoothness of `f` on that set can be expressed by purely looking in +these charts. +Note: this lemma uses `extChartAt I x '' s` instead of `(extChartAt I x).symm ⁻¹' s` to ensure +that this set lies in `(extChartAt I x).target`. -/ theorem mdifferentiableOn_iff_of_subset_source {x : M} {y : M'} (hs : s ⊆ (chartAt H x).source) (h2s : MapsTo f s (chartAt H' y).source) : MDifferentiableOn I I' f s ↔ @@ -378,10 +378,10 @@ theorem mdifferentiableOn_iff_of_subset_source {x : M} {y : M'} (hs : s ⊆ (cha (chart_mem_maximalAtlas y) hs h2s /-- If the set where you want `f` to be smooth lies entirely in a single chart, and `f` maps it - into a single chart, the smoothness of `f` on that set can be expressed by purely looking in - these charts. - Note: this lemma uses `extChartAt I x '' s` instead of `(extChartAt I x).symm ⁻¹' s` to ensure - that this set lies in `(extChartAt I x).target`. -/ +into a single chart, the smoothness of `f` on that set can be expressed by purely looking in +these charts. +Note: this lemma uses `extChartAt I x '' s` instead of `(extChartAt I x).symm ⁻¹' s` to ensure +that this set lies in `(extChartAt I x).target`. -/ theorem mdifferentiableOn_iff_of_subset_source' {x : M} {y : M'} (hs : s ⊆ (extChartAt I x).source) (h2s : MapsTo f s (extChartAt I' y).source) : MDifferentiableOn I I' f s ↔ diff --git a/Mathlib/Geometry/Manifold/PartitionOfUnity.lean b/Mathlib/Geometry/Manifold/PartitionOfUnity.lean index 9b52a1a42507b..32de568cb6743 100644 --- a/Mathlib/Geometry/Manifold/PartitionOfUnity.lean +++ b/Mathlib/Geometry/Manifold/PartitionOfUnity.lean @@ -213,7 +213,7 @@ section finsupport variable {s : Set M} (ρ : SmoothPartitionOfUnity ι I M s) (x₀ : M) /-- The support of a smooth partition of unity at a point `x₀` as a `Finset`. - This is the set of `i : ι` such that `x₀ ∈ support f i`, i.e. `f i ≠ x₀`. -/ +This is the set of `i : ι` such that `x₀ ∈ support f i`, i.e. `f i ≠ x₀`. -/ def finsupport : Finset ι := ρ.toPartitionOfUnity.finsupport x₀ @[simp] @@ -245,7 +245,7 @@ theorem finite_tsupport : {i | x₀ ∈ tsupport (ρ i)}.Finite := ρ.toPartitionOfUnity.finite_tsupport _ /-- The tsupport of a partition of unity at a point `x₀` as a `Finset`. - This is the set of `i : ι` such that `x₀ ∈ tsupport f i`. -/ +This is the set of `i : ι` such that `x₀ ∈ tsupport f i`. -/ def fintsupport (x : M) : Finset ι := (ρ.finite_tsupport x).toFinset