diff --git a/Mathlib/Algebra/Category/AlgCat/Monoidal.lean b/Mathlib/Algebra/Category/AlgCat/Monoidal.lean index e2b40f3b548134..354ca7df7689f2 100644 --- a/Mathlib/Algebra/Category/AlgCat/Monoidal.lean +++ b/Mathlib/Algebra/Category/AlgCat/Monoidal.lean @@ -43,8 +43,6 @@ noncomputable abbrev tensorHom {W X Y Z : AlgCat.{u} R} (f : W ⟶ X) (g : Y ⟶ tensorObj W Y ⟶ tensorObj X Z := ofHom <| Algebra.TensorProduct.map f.hom g.hom -open MonoidalCategory - end instMonoidalCategory open instMonoidalCategory diff --git a/Mathlib/Algebra/Group/Equiv/Basic.lean b/Mathlib/Algebra/Group/Equiv/Basic.lean index fef7e59a021acb..ba1e4c2d29cb53 100644 --- a/Mathlib/Algebra/Group/Equiv/Basic.lean +++ b/Mathlib/Algebra/Group/Equiv/Basic.lean @@ -28,11 +28,6 @@ open Function variable {F α β M M₁ M₂ M₃ N N₁ N₂ N₃ P Q G H : Type*} -namespace EmbeddingLike -variable [One M] [One N] [FunLike F M N] [EmbeddingLike F M N] [OneHomClass F M N] - -end EmbeddingLike - variable [EquivLike F α β] @[to_additive] diff --git a/Mathlib/Algebra/Group/Pointwise/Finset/Scalar.lean b/Mathlib/Algebra/Group/Pointwise/Finset/Scalar.lean index 3dfae13784e895..14b084989b0684 100644 --- a/Mathlib/Algebra/Group/Pointwise/Finset/Scalar.lean +++ b/Mathlib/Algebra/Group/Pointwise/Finset/Scalar.lean @@ -340,26 +340,6 @@ theorem op_smul_finset_smul_eq_smul_smul_finset (a : α) (s : Finset β) (t : Fi end SMul - -section IsRightCancelMul - -variable [Mul α] [IsRightCancelMul α] [DecidableEq α] {s t : Finset α} {a : α} - - -end IsRightCancelMul - -section CancelMonoid -variable [DecidableEq α] [CancelMonoid α] {s : Finset α} {m n : ℕ} - - -end CancelMonoid - -section Group -variable [Group α] [DecidableEq α] {s t : Finset α} - - -end Group - @[to_additive] theorem image_smul_comm [DecidableEq β] [DecidableEq γ] [SMul α β] [SMul α γ] (f : β → γ) (a : α) (s : Finset β) : (∀ b, f (a • b) = a • f b) → (a • s).image f = a • s.image f := @@ -367,12 +347,6 @@ theorem image_smul_comm [DecidableEq β] [DecidableEq γ] [SMul α β] [SMul α end Finset -namespace Fintype -variable {ι : Type*} {α β : ι → Type*} [Fintype ι] [DecidableEq ι] [∀ i, DecidableEq (β i)] - [∀ i, DecidableEq (α i)] - -end Fintype - open Pointwise namespace Set diff --git a/Mathlib/Algebra/Group/Subgroup/Basic.lean b/Mathlib/Algebra/Group/Subgroup/Basic.lean index 059694529744ea..2066ab169657ca 100644 --- a/Mathlib/Algebra/Group/Subgroup/Basic.lean +++ b/Mathlib/Algebra/Group/Subgroup/Basic.lean @@ -403,8 +403,6 @@ theorem _root_.normalizerCondition_iff_only_full_group_self_normalizing : simp only [lt_iff_le_and_ne, le_normalizer, le_top, Ne] tauto -variable (H) - end Normalizer end Subgroup diff --git a/Mathlib/Algebra/Group/Submonoid/Membership.lean b/Mathlib/Algebra/Group/Submonoid/Membership.lean index d6a3701987a1bf..b8a42229942f77 100644 --- a/Mathlib/Algebra/Group/Submonoid/Membership.lean +++ b/Mathlib/Algebra/Group/Submonoid/Membership.lean @@ -42,12 +42,6 @@ assert_not_exists MonoidWithZero variable {M A B : Type*} -section Assoc - -variable [Monoid M] [SetLike B M] [SubmonoidClass B M] {S : B} - -end Assoc - section NonAssoc variable [MulOneClass M] diff --git a/Mathlib/Algebra/GroupWithZero/Units/Basic.lean b/Mathlib/Algebra/GroupWithZero/Units/Basic.lean index 1432e5afe85e79..a9671fa8a4e4ff 100644 --- a/Mathlib/Algebra/GroupWithZero/Units/Basic.lean +++ b/Mathlib/Algebra/GroupWithZero/Units/Basic.lean @@ -133,8 +133,6 @@ theorem inverse_zero : inverse (0 : M₀) = 0 := by nontriviality exact inverse_non_unit _ not_isUnit_zero -variable {M₀} - end Ring theorem IsUnit.ringInverse {a : M₀} : IsUnit a → IsUnit (Ring.inverse a) diff --git a/Mathlib/Algebra/Module/RingHom.lean b/Mathlib/Algebra/Module/RingHom.lean index 429fc4fbcfccd2..4ab06dbbb31037 100644 --- a/Mathlib/Algebra/Module/RingHom.lean +++ b/Mathlib/Algebra/Module/RingHom.lean @@ -63,8 +63,6 @@ abbrev Module.compHom [Semiring S] (f : S →+* R) : Module S M := -- TODO(jmc): there should be a rw-lemma `smul_comp` close to `SMulZeroClass.compFun` add_smul := fun r s x => show f (r + s) • x = f r • x + f s • x by simp [add_smul] } -variable {M} - end AddCommMonoid /-- A ring homomorphism `f : R →+* M` defines a module structure by `r • x = f r * x`. diff --git a/Mathlib/Algebra/Order/GroupWithZero/Unbundled/Basic.lean b/Mathlib/Algebra/Order/GroupWithZero/Unbundled/Basic.lean index 8093162328db04..d29c9c325c09b3 100644 --- a/Mathlib/Algebra/Order/GroupWithZero/Unbundled/Basic.lean +++ b/Mathlib/Algebra/Order/GroupWithZero/Unbundled/Basic.lean @@ -1344,8 +1344,6 @@ lemma zpow_lt_zpow_iff_left₀ (ha : 0 ≤ a) (hb : 0 ≤ b) (hn : 0 < n) : a ^ end MulPosMono -variable [MulPosStrictMono G₀] - end GroupWithZero.LinearOrder section CommGroupWithZero diff --git a/Mathlib/AlgebraicGeometry/AffineScheme.lean b/Mathlib/AlgebraicGeometry/AffineScheme.lean index 95673ed11c068c..9f4ed883920d7d 100644 --- a/Mathlib/AlgebraicGeometry/AffineScheme.lean +++ b/Mathlib/AlgebraicGeometry/AffineScheme.lean @@ -1216,8 +1216,6 @@ lemma specTargetImageFactorization_comp : specTargetImageFactorization f ≫ Spec.map (specTargetImageRingHom f) = f := f.liftQuotient_comp _ _ -open RingHom - end Factorization section Stalks diff --git a/Mathlib/AlgebraicTopology/SimplicialSet/HoFunctorMonoidal.lean b/Mathlib/AlgebraicTopology/SimplicialSet/HoFunctorMonoidal.lean index a7600141518638..a9eda8eba2813a 100644 --- a/Mathlib/AlgebraicTopology/SimplicialSet/HoFunctorMonoidal.lean +++ b/Mathlib/AlgebraicTopology/SimplicialSet/HoFunctorMonoidal.lean @@ -399,8 +399,6 @@ instance : hoFunctor₂.{u}.Monoidal := instance hoFunctor.monoidal : hoFunctor.{u}.Monoidal := inferInstanceAs (truncation 2 ⋙ hoFunctor₂).Monoidal -open MonoidalCategory - end Truncated /-- An equivalence between the vertices of a simplicial set `X` and the diff --git a/Mathlib/Analysis/Asymptotics/SuperpolynomialDecay.lean b/Mathlib/Analysis/Asymptotics/SuperpolynomialDecay.lean index eee9e80e47da23..b1001051c200d5 100644 --- a/Mathlib/Analysis/Asymptotics/SuperpolynomialDecay.lean +++ b/Mathlib/Analysis/Asymptotics/SuperpolynomialDecay.lean @@ -187,8 +187,6 @@ theorem superpolynomialDecay_const_mul_iff [ContinuousMul β] {c : β} (hc0 : c ⟨fun h => (h.const_mul c⁻¹).congr fun x => by simp [← mul_assoc, inv_mul_cancel₀ hc0], fun h => h.const_mul c⟩ -variable {l k f} - end Field section LinearOrderedField @@ -272,8 +270,6 @@ theorem superpolynomialDecay_mul_param_pow_iff (hk : Tendsto k l atTop) (n : ℕ SuperpolynomialDecay l k (f * k ^ n) ↔ SuperpolynomialDecay l k f := by simpa [mul_comm f] using superpolynomialDecay_param_pow_mul_iff f hk n -variable {f} - end LinearOrderedField section NormedLinearOrderedField diff --git a/Mathlib/Analysis/Calculus/BumpFunction/FiniteDimension.lean b/Mathlib/Analysis/Calculus/BumpFunction/FiniteDimension.lean index eb848c1a2f2ab9..386698c4e8bdc4 100644 --- a/Mathlib/Analysis/Calculus/BumpFunction/FiniteDimension.lean +++ b/Mathlib/Analysis/Calculus/BumpFunction/FiniteDimension.lean @@ -459,8 +459,6 @@ theorem y_support {D : ℝ} (Dpos : 0 < D) (D_lt_one : D < 1) : ⟨fun _ hx => (y_pos_of_mem_ball Dpos D_lt_one hx).ne', fun _ hx => y_eq_zero_of_notMem_ball Dpos hx⟩ -variable {E} - end HelperDefinitions instance (priority := 100) {E : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E] diff --git a/Mathlib/Analysis/Calculus/LineDeriv/Basic.lean b/Mathlib/Analysis/Calculus/LineDeriv/Basic.lean index 2d58123d708550..fe86d614d1312f 100644 --- a/Mathlib/Analysis/Calculus/LineDeriv/Basic.lean +++ b/Mathlib/Analysis/Calculus/LineDeriv/Basic.lean @@ -451,8 +451,6 @@ theorem norm_lineDeriv_le_of_lipschitz {f : E → F} {x₀ : E} {C : ℝ≥0} (hlip : LipschitzWith C f) : ‖lineDeriv 𝕜 f x₀ v‖ ≤ C * ‖v‖ := norm_lineDeriv_le_of_lipschitzOn 𝕜 univ_mem (lipschitzOnWith_univ.2 hlip) -variable {𝕜} - end NormedSpace section Zero diff --git a/Mathlib/Analysis/Convex/Cone/InnerDual.lean b/Mathlib/Analysis/Convex/Cone/InnerDual.lean index eba8392b32748f..22a01234e4929f 100644 --- a/Mathlib/Analysis/Convex/Cone/InnerDual.lean +++ b/Mathlib/Analysis/Convex/Cone/InnerDual.lean @@ -186,11 +186,6 @@ theorem ConvexCone.hyperplane_separation_of_nonempty_of_isClosed_of_notMem (K : _ = ⟪b - z, b - z + z⟫_ℝ := (inner_add_right _ _ _).symm _ = ⟪b - z, b⟫_ℝ := by rw [sub_add_cancel] -namespace ProperCone -variable {F : Type*} [NormedAddCommGroup F] [InnerProductSpace ℝ F] - -end ProperCone - end CompleteSpace end Dual diff --git a/Mathlib/Analysis/Distribution/SchwartzSpace.lean b/Mathlib/Analysis/Distribution/SchwartzSpace.lean index c636e5b8664d16..cb904567e7ecf9 100644 --- a/Mathlib/Analysis/Distribution/SchwartzSpace.lean +++ b/Mathlib/Analysis/Distribution/SchwartzSpace.lean @@ -1227,8 +1227,6 @@ theorem toBoundedContinuousFunctionCLM_apply (f : 𝓢(E, F)) (x : E) : toBoundedContinuousFunctionCLM 𝕜 E F f x = f x := rfl -variable {E} - end BoundedContinuousFunction section ZeroAtInfty diff --git a/Mathlib/Analysis/Normed/Module/Alternating/Basic.lean b/Mathlib/Analysis/Normed/Module/Alternating/Basic.lean index 2629bfca5d0a42..187cb92ebc337d 100644 --- a/Mathlib/Analysis/Normed/Module/Alternating/Basic.lean +++ b/Mathlib/Analysis/Normed/Module/Alternating/Basic.lean @@ -365,8 +365,6 @@ def restrictScalarsLI : E [⋀^ι]→L[𝕜] F →ₗᵢ[𝕜'] E [⋀^ι]→L[ map_smul' _ _ := rfl norm_map' _ := rfl -variable {𝕜'} - end restrictScalars /-- The difference `f m₁ - f m₂` is controlled in terms of `‖f‖` and `‖m₁ - m₂‖`, precise version. diff --git a/Mathlib/CategoryTheory/Limits/Shapes/IsTerminal.lean b/Mathlib/CategoryTheory/Limits/Shapes/IsTerminal.lean index fa1ef79c442401..ea1f97c858a671 100644 --- a/Mathlib/CategoryTheory/Limits/Shapes/IsTerminal.lean +++ b/Mathlib/CategoryTheory/Limits/Shapes/IsTerminal.lean @@ -334,12 +334,6 @@ theorem InitialMonoClass.of_isTerminal {I T : C} (hI : IsInitial I) (hT : IsTerm (_ : Mono (hI.to T)) : InitialMonoClass C := InitialMonoClass.of_isInitial hI fun X => mono_of_mono_fac (hI.hom_ext (_ ≫ hT.from X) (hI.to T)) -section Comparison - -variable {D : Type u₂} [Category.{v₂} D] (G : C ⥤ D) - -end Comparison - variable {J : Type u} [Category.{v} J] /-- From a functor `F : J ⥤ C`, given an initial object of `J`, construct a cone for `J`. diff --git a/Mathlib/CategoryTheory/Noetherian.lean b/Mathlib/CategoryTheory/Noetherian.lean index 794402ed9f2a86..ccf313f37f67d1 100644 --- a/Mathlib/CategoryTheory/Noetherian.lean +++ b/Mathlib/CategoryTheory/Noetherian.lean @@ -45,6 +45,4 @@ class Artinian : Prop extends EssentiallySmall C where attribute [instance] Artinian.isArtinianObject -open Subobject - end CategoryTheory diff --git a/Mathlib/CategoryTheory/Sites/Canonical.lean b/Mathlib/CategoryTheory/Sites/Canonical.lean index 817b1da46d97c6..2a42bf3d62ed34 100644 --- a/Mathlib/CategoryTheory/Sites/Canonical.lean +++ b/Mathlib/CategoryTheory/Sites/Canonical.lean @@ -229,8 +229,6 @@ theorem isSheaf_of_isRepresentable {J : GrothendieckTopology C} [Subcanonical J] (P : Cᵒᵖ ⥤ Type v) [P.IsRepresentable] : Presieve.IsSheaf J P := Presieve.isSheaf_of_le _ J.le_canonical (Sheaf.isSheaf_of_isRepresentable P) -variable {J : GrothendieckTopology C} - end Subcanonical variable (J : GrothendieckTopology C) diff --git a/Mathlib/Control/LawfulFix.lean b/Mathlib/Control/LawfulFix.lean index 2012a5ca54a063..64ee89d87aa87f 100644 --- a/Mathlib/Control/LawfulFix.lean +++ b/Mathlib/Control/LawfulFix.lean @@ -165,8 +165,6 @@ theorem fix_eq_of_ωScottContinuous (hc : ωScottContinuous g) : intro i exists i.succ -variable {f} - end Part namespace Part diff --git a/Mathlib/Data/Matrix/Basic.lean b/Mathlib/Data/Matrix/Basic.lean index 431db9e5f655fe..4f1d1dc2723c37 100644 --- a/Mathlib/Data/Matrix/Basic.lean +++ b/Mathlib/Data/Matrix/Basic.lean @@ -157,12 +157,6 @@ end Diag open Matrix -section AddCommMonoid - -variable [AddCommMonoid α] [Mul α] - -end AddCommMonoid - section NonAssocSemiring variable [NonAssocSemiring α] diff --git a/Mathlib/Data/Matrix/Mul.lean b/Mathlib/Data/Matrix/Mul.lean index c1e871134388cb..bbed2bc75580a8 100644 --- a/Mathlib/Data/Matrix/Mul.lean +++ b/Mathlib/Data/Matrix/Mul.lean @@ -472,8 +472,6 @@ theorem op_smul_one_eq_diagonal [DecidableEq m] (a : α) : MulOpposite.op a • (1 : Matrix m m α) = diagonal fun _ => a := by simp_rw [← diagonal_one, ← diagonal_smul, Pi.smul_def, op_smul_eq_mul, one_mul] -variable (α n) - end NonAssocSemiring section NonUnitalSemiring @@ -1152,8 +1150,6 @@ theorem transpose_mul [AddCommMonoid α] [CommMagma α] [Fintype n] (M : Matrix ext apply dotProduct_comm -variable (m n α) - end Transpose theorem submatrix_mul [Fintype n] [Fintype o] [Mul α] [AddCommMonoid α] {p q : Type*} diff --git a/Mathlib/Data/Tree/RBMap.lean b/Mathlib/Data/Tree/RBMap.lean index 6c42cfb78dd450..f478aac349c1ab 100644 --- a/Mathlib/Data/Tree/RBMap.lean +++ b/Mathlib/Data/Tree/RBMap.lean @@ -21,13 +21,3 @@ Implement a `Traversable` instance for `Tree`. -/ - -public section - -namespace Tree - -universe u - -variable {α : Type u} - -end Tree diff --git a/Mathlib/GroupTheory/Congruence/Defs.lean b/Mathlib/GroupTheory/Congruence/Defs.lean index 566e8c86f2b289..e75ac03cf2eeb9 100644 --- a/Mathlib/GroupTheory/Congruence/Defs.lean +++ b/Mathlib/GroupTheory/Congruence/Defs.lean @@ -505,12 +505,6 @@ theorem comap_rel {f : M → N} (H : ∀ x y, f (x * y) = f x * f y) {c : Con N} comap f H c x y ↔ c (f x) (f y) := Iff.rfl -section - -open Quotient - -end - end section MulOneClass diff --git a/Mathlib/LinearAlgebra/FiniteDimensional/Basic.lean b/Mathlib/LinearAlgebra/FiniteDimensional/Basic.lean index ed088e70e76e38..efd41859ba2c53 100644 --- a/Mathlib/LinearAlgebra/FiniteDimensional/Basic.lean +++ b/Mathlib/LinearAlgebra/FiniteDimensional/Basic.lean @@ -155,8 +155,6 @@ variable (K V) instance finiteDimensional_bot : FiniteDimensional K (⊥ : Submodule K V) := .of_rank_eq_zero <| by simp -variable {K V} - end ZeroRank namespace Submodule diff --git a/Mathlib/LinearAlgebra/QuadraticForm/QuadraticModuleCat/Monoidal.lean b/Mathlib/LinearAlgebra/QuadraticForm/QuadraticModuleCat/Monoidal.lean index bcc94d349e9496..67ce6df3c0a2a3 100644 --- a/Mathlib/LinearAlgebra/QuadraticForm/QuadraticModuleCat/Monoidal.lean +++ b/Mathlib/LinearAlgebra/QuadraticForm/QuadraticModuleCat/Monoidal.lean @@ -53,8 +53,6 @@ abbrev tensorHom {W X Y Z : QuadraticModuleCat.{u} R} (f : W ⟶ X) (g : Y ⟶ Z tensorObj W Y ⟶ tensorObj X Z := ⟨f.toIsometry.tmul g.toIsometry⟩ -open MonoidalCategory - end instMonoidalCategory open instMonoidalCategory diff --git a/Mathlib/LinearAlgebra/TensorAlgebra/Basic.lean b/Mathlib/LinearAlgebra/TensorAlgebra/Basic.lean index ac65ec59805bae..be00ad4787c5b0 100644 --- a/Mathlib/LinearAlgebra/TensorAlgebra/Basic.lean +++ b/Mathlib/LinearAlgebra/TensorAlgebra/Basic.lean @@ -316,8 +316,6 @@ def tprod (n : ℕ) : MultilinearMap R (fun _ : Fin n => M) (TensorAlgebra R M) theorem tprod_apply {n : ℕ} (x : Fin n → M) : tprod R M n x = (List.ofFn fun i => ι R (x i)).prod := rfl -variable {R M} - end TensorAlgebra namespace FreeAlgebra diff --git a/Mathlib/MeasureTheory/Function/AEEqOfIntegral.lean b/Mathlib/MeasureTheory/Function/AEEqOfIntegral.lean index 1ba645d3c6d6c9..ec9e0a6c64840b 100644 --- a/Mathlib/MeasureTheory/Function/AEEqOfIntegral.lean +++ b/Mathlib/MeasureTheory/Function/AEEqOfIntegral.lean @@ -115,8 +115,6 @@ theorem ae_eq_zero_of_forall_dual [NormedAddCommGroup E] [NormedSpace 𝕜 E] ae_eq_zero_of_forall_dual_of_isSeparable 𝕜 (.of_separableSpace Set.univ) hf (Eventually.of_forall fun _ => Set.mem_univ _) -variable {𝕜} - end AeEqOfForall variable {α E : Type*} {m m0 : MeasurableSpace α} {μ : Measure α} diff --git a/Mathlib/MeasureTheory/Function/SimpleFuncDenseLp.lean b/Mathlib/MeasureTheory/Function/SimpleFuncDenseLp.lean index 23611b10ac1e3a..bb5d345cab7b04 100644 --- a/Mathlib/MeasureTheory/Function/SimpleFuncDenseLp.lean +++ b/Mathlib/MeasureTheory/Function/SimpleFuncDenseLp.lean @@ -695,8 +695,6 @@ def coeToLp : Lp.simpleFunc E p μ →L[𝕜] Lp E p μ := map_smul' := fun _ _ => rfl cont := Lp.simpleFunc.uniformContinuous.continuous } -variable {α E 𝕜} - end CoeToLp section Order @@ -789,8 +787,6 @@ theorem denseRange_coeSimpleFuncNonnegToLpNonneg [hp : Fact (1 ≤ p)] (hp_ne_to exact h_toLp n · rfl -variable {p μ G} - end Order end simpleFunc diff --git a/Mathlib/MeasureTheory/Integral/Prod.lean b/Mathlib/MeasureTheory/Integral/Prod.lean index 4cba649d7f533a..184104dac5a778 100644 --- a/Mathlib/MeasureTheory/Integral/Prod.lean +++ b/Mathlib/MeasureTheory/Integral/Prod.lean @@ -162,8 +162,6 @@ theorem integrable_measure_prodMk_left {s : Set (α × β)} (hs : MeasurableSet end Measure -open Measure - end MeasureTheory open MeasureTheory.Measure diff --git a/Mathlib/NumberTheory/Padics/PadicNumbers.lean b/Mathlib/NumberTheory/Padics/PadicNumbers.lean index 71575d1e64a04e..9f56d64a7a937d 100644 --- a/Mathlib/NumberTheory/Padics/PadicNumbers.lean +++ b/Mathlib/NumberTheory/Padics/PadicNumbers.lean @@ -321,12 +321,13 @@ end Valuation end PadicSeq +-- Porting note: Commented out `padic_index_simp` tactic + +/- section open PadicSeq --- Porting note: Commented out `padic_index_simp` tactic -/- private unsafe def index_simp_core (hh hf hg : expr) (at_ : Interactive.Loc := Interactive.Loc.ns [none]) : tactic Unit := do let [v1, v2, v3] ← [hh, hf, hg].mapM fun n => tactic.mk_app `` stationary_point [n] <|> return n @@ -344,9 +345,9 @@ unsafe def tactic.interactive.padic_index_simp (l : interactive.parse interactiv (at_ : interactive.parse interactive.types.location) : tactic Unit := do let [h, f, g] ← l.mapM tactic.i_to_expr index_simp_core h f g at_ --/ end +-/ namespace PadicSeq diff --git a/Mathlib/Order/Filter/AtTopBot/Monoid.lean b/Mathlib/Order/Filter/AtTopBot/Monoid.lean index 0acb403ff80937..e5c549500cbe3e 100644 --- a/Mathlib/Order/Filter/AtTopBot/Monoid.lean +++ b/Mathlib/Order/Filter/AtTopBot/Monoid.lean @@ -171,11 +171,4 @@ theorem Tendsto.atBot_of_mul_const_le (hg : ∃ C, ∀ x, C ≤ g x) end OrderedCancelCommMonoid -section OrderedCancelAddCommMonoid - -variable [AddCommMonoid M] [PartialOrder M] [IsOrderedCancelAddMonoid M] - {l : Filter α} {f g : α → M} - -end OrderedCancelAddCommMonoid - end Filter diff --git a/Mathlib/RepresentationTheory/Homological/GroupCohomology/Basic.lean b/Mathlib/RepresentationTheory/Homological/GroupCohomology/Basic.lean index b097fe6b5e062c..13a830078ad5d9 100644 --- a/Mathlib/RepresentationTheory/Homological/GroupCohomology/Basic.lean +++ b/Mathlib/RepresentationTheory/Homological/GroupCohomology/Basic.lean @@ -76,15 +76,9 @@ variable {k G : Type u} [CommRing k] {n : ℕ} open CategoryTheory -namespace groupCohomology - -variable [Monoid G] - -end groupCohomology - namespace inhomogeneousCochains -open Rep groupCohomology +open Rep /-- The differential in the complex of inhomogeneous cochains used to calculate group cohomology. -/ diff --git a/Mathlib/RingTheory/NonUnitalSubsemiring/Defs.lean b/Mathlib/RingTheory/NonUnitalSubsemiring/Defs.lean index 63875b3e3484dd..ef5ce612d82f0f 100644 --- a/Mathlib/RingTheory/NonUnitalSubsemiring/Defs.lean +++ b/Mathlib/RingTheory/NonUnitalSubsemiring/Defs.lean @@ -271,16 +271,6 @@ lemma toAddSubmonoid_eq_top {S : NonUnitalSubsemiring R} : S.toAddSubmonoid = end NonUnitalSubsemiring -namespace NonUnitalRingHom - -open NonUnitalSubsemiring - -variable [NonUnitalNonAssocSemiring S] -variable {F : Type*} [FunLike F R S] [NonUnitalRingHomClass F R S] -variable (f : F) - -end NonUnitalRingHom - namespace NonUnitalSubsemiring -- should we define this as the range of the zero homomorphism? diff --git a/Mathlib/Topology/Algebra/IsUniformGroup/Defs.lean b/Mathlib/Topology/Algebra/IsUniformGroup/Defs.lean index 761dae2d89088c..d90be8b8dce894 100644 --- a/Mathlib/Topology/Algebra/IsUniformGroup/Defs.lean +++ b/Mathlib/Topology/Algebra/IsUniformGroup/Defs.lean @@ -642,7 +642,6 @@ theorem isUniformGroup_of_commGroup : IsUniformGroup G := by exact (continuous_div'.tendsto' 1 1 (div_one 1)).comp tendsto_comap alias comm_topologicalGroup_is_uniform := isUniformGroup_of_commGroup -open Set end diff --git a/Mathlib/Topology/DiscreteQuotient.lean b/Mathlib/Topology/DiscreteQuotient.lean index 90471559910fe9..61488ab579f959 100644 --- a/Mathlib/Topology/DiscreteQuotient.lean +++ b/Mathlib/Topology/DiscreteQuotient.lean @@ -392,8 +392,6 @@ TODO: show that this is precisely those finsets of clopens which form a partitio noncomputable def equivFinsetClopens [CompactSpace X] := Equiv.ofInjective _ (finsetClopens_inj X) -variable {X} - end DiscreteQuotient namespace LocallyConstant diff --git a/Mathlib/Topology/MetricSpace/Lipschitz.lean b/Mathlib/Topology/MetricSpace/Lipschitz.lean index 9ae7b358741cb4..e498fc5af9bfe5 100644 --- a/Mathlib/Topology/MetricSpace/Lipschitz.lean +++ b/Mathlib/Topology/MetricSpace/Lipschitz.lean @@ -208,12 +208,6 @@ lemma LipschitzWith.properSpace {X Y : Type*} [PseudoMetricSpace X] ⟨fun x r ↦ (hf.isCompact_preimage (isCompact_closedBall (f x) (K * r))).of_isClosed_subset Metric.isClosed_closedBall (hf'.mapsTo_closedBall x r).subset_preimage⟩ -namespace Metric - -variable [PseudoMetricSpace α] [PseudoMetricSpace β] {s : Set α} {t : Set β} - -end Metric - namespace LipschitzOnWith section Metric diff --git a/Mathlib/Topology/Semicontinuity/Basic.lean b/Mathlib/Topology/Semicontinuity/Basic.lean index c1174104ad8fd9..487094f2376348 100644 --- a/Mathlib/Topology/Semicontinuity/Basic.lean +++ b/Mathlib/Topology/Semicontinuity/Basic.lean @@ -596,8 +596,6 @@ theorem LowerSemicontinuous.inf (hf : LowerSemicontinuous f) LowerSemicontinuous fun x ↦ f x ⊓ g x := fun a ↦ LowerSemicontinuousAt.inf (hf a) (hg a) -variable {ι : Type*} {f : ι → α → β} {a : α} {I : Set ι} - end section diff --git a/Mathlib/Topology/Separation/Regular.lean b/Mathlib/Topology/Separation/Regular.lean index 0bfe90c63fc6be..f262261df8a204 100644 --- a/Mathlib/Topology/Separation/Regular.lean +++ b/Mathlib/Topology/Separation/Regular.lean @@ -549,8 +549,6 @@ instance [NormalSpace X] : NormalSpace (SeparationQuotient X) where end SeparationQuotient -variable (X) - end Normality section CompletelyNormal