Commit 2023-11-08 06:59 4a70d87f

View on Github →

chore: move TopologicalSpace.SecondCountableTopology into the root namespace (#8186) All the other properties of topological spaces like T0Space or RegularSpace are in the root namespace. Many files were opening TopologicalSpace just for the sake of shortening TopologicalSpace.SecondCountableTopology...

Estimated changes

Modified Mathlib/Analysis/Calculus/LineDeriv/Measurable.lean

Modified Mathlib/Analysis/Complex/UpperHalfPlane/Topology.lean

Modified Mathlib/Analysis/Distribution/SchwartzSpace.lean

Modified Mathlib/Analysis/Fourier/FourierTransform.lean

modified theorem VectorFourier.fourierIntegral_continuous

Modified Mathlib/Analysis/LocallyConvex/WithSeminorms.lean

Modified Mathlib/MeasureTheory/Function/SpecialFunctions/Inner.lean

Modified Mathlib/MeasureTheory/Integral/BoundedContinuousFunction.lean

Modified Mathlib/MeasureTheory/Integral/FundThmCalculus.lean

Modified Mathlib/MeasureTheory/Integral/IntervalIntegral.lean

Modified Mathlib/MeasureTheory/Integral/LebesgueNormedSpace.lean

Modified Mathlib/MeasureTheory/Measure/Hausdorff.lean

Modified Mathlib/MeasureTheory/Measure/MeasureSpace.lean

Modified Mathlib/MeasureTheory/Measure/OuterMeasure.lean

Modified Mathlib/MeasureTheory/Measure/Regular.lean

Modified Mathlib/Topology/Algebra/InfiniteSum/Basic.lean

modified theorem Summable.countable_support

Modified Mathlib/Topology/Algebra/Order/LeftRightLim.lean

modified theorem Antitone.countable_not_continuousAt

modified theorem Monotone.countable_not_continuousAt

modified theorem Monotone.countable_not_continuousWithinAt_Iio

modified theorem Monotone.countable_not_continuousWithinAt_Ioi

Modified Mathlib/Topology/Bases.lean

Modified Mathlib/Topology/Homeomorph.lean

Modified Mathlib/Topology/Instances/NNReal.lean

Modified Mathlib/Topology/LocalHomeomorph.lean

Modified Mathlib/Topology/Metrizable/Basic.lean

Modified Mathlib/Topology/Order/Basic.lean

added theorem SecondCountableTopology.of_separableSpace_orderTopology

deleted theorem TopologicalSpace.SecondCountableTopology.of_separableSpace_orderTopology

Modified Mathlib/Topology/Sequences.lean