Commit 2025-01-13 14:29 3aa8ab5d

View on Github →

chore: split Mathlib.Topology.Instances.*Real (#20707) Splits each of these files for Real/EReal/NNReal/ENNReal into a Defs file, containing all the instances and minimal imports, and a Lemmas file with all the remaining current content.

Estimated changes

Modified Mathlib.lean

Modified Mathlib/AlgebraicTopology/TopologicalSimplex.lean

Modified Mathlib/Analysis/Asymptotics/TVS.lean

Modified Mathlib/Analysis/Complex/HalfPlane.lean

Modified Mathlib/Analysis/Normed/Field/Lemmas.lean

Modified Mathlib/Analysis/Normed/Group/InfiniteSum.lean

Modified Mathlib/Analysis/Normed/Group/Lemmas.lean

Modified Mathlib/Analysis/Normed/Group/Quotient.lean

Modified Mathlib/Analysis/NormedSpace/FunctionSeries.lean

Modified Mathlib/Analysis/SpecificLimits/Basic.lean

Modified Mathlib/Analysis/SpecificLimits/Normed.lean

Modified Mathlib/Analysis/Subadditive.lean

Modified Mathlib/Analysis/SumOverResidueClass.lean

Modified Mathlib/Data/Complex/Exponential.lean

Modified Mathlib/Data/Complex/FiniteDimensional.lean

Modified Mathlib/Data/Real/Sqrt.lean

Modified Mathlib/Dynamics/Circle/RotationNumber/TranslationNumber.lean

Modified Mathlib/MeasureTheory/Constructions/BorelSpace/Basic.lean

Modified Mathlib/MeasureTheory/Constructions/BorelSpace/Real.lean

Modified Mathlib/MeasureTheory/Decomposition/Jordan.lean

Modified Mathlib/MeasureTheory/Integral/VitaliCaratheodory.lean

Modified Mathlib/MeasureTheory/Measure/Stieltjes.lean

Modified Mathlib/MeasureTheory/OuterMeasure/Basic.lean

Modified Mathlib/MeasureTheory/OuterMeasure/Defs.lean

Modified Mathlib/Order/Filter/ENNReal.lean

Modified Mathlib/Probability/ProbabilityMassFunction/Basic.lean

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

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

Modified Mathlib/Topology/Algebra/Module/Multilinear/Topology.lean

Modified Mathlib/Topology/Instances/CantorSet.lean

Created Mathlib/Topology/Instances/ENNReal/Defs.lean

added theorem ENNReal.isEmbedding_coe

added theorem ENNReal.isOpenEmbedding_coe

added theorem ENNReal.nhds_coe_coe

added theorem ENNReal.tendsto_coe

Renamed Mathlib/Topology/Instances/ENNReal.lean to Mathlib/Topology/Instances/ENNReal/Lemmas.lean

deleted theorem ENNReal.isEmbedding_coe

deleted theorem ENNReal.isOpenEmbedding_coe

deleted theorem ENNReal.nhds_coe_coe

deleted theorem ENNReal.tendsto_coe

Created Mathlib/Topology/Instances/EReal/Defs.lean

added theorem EReal.denseRange_ratCast

Renamed Mathlib/Topology/Instances/EReal.lean to Mathlib/Topology/Instances/EReal/Lemmas.lean

deleted theorem EReal.denseRange_ratCast

Modified Mathlib/Topology/Instances/Irrational.lean

Created Mathlib/Topology/Instances/NNReal/Defs.lean

added def ContinuousMap.coeNNRealReal

added theorem NNReal.continuous_coe

Renamed Mathlib/Topology/Instances/NNReal.lean to Mathlib/Topology/Instances/NNReal/Lemmas.lean

deleted def ContinuousMap.coeNNRealReal

deleted theorem NNReal.continuous_coe

Modified Mathlib/Topology/Instances/Rat.lean

Created Mathlib/Topology/Instances/Real/Defs.lean

added theorem Real.uniformContinuous_add

added theorem Real.uniformContinuous_neg

Renamed Mathlib/Topology/Instances/Real.lean to Mathlib/Topology/Instances/Real/Lemmas.lean

deleted theorem Real.uniformContinuous_add

deleted theorem Real.uniformContinuous_neg

Modified Mathlib/Topology/Instances/ZMultiples.lean

Modified Mathlib/Topology/MetricSpace/Completion.lean

Modified Mathlib/Topology/MetricSpace/PartitionOfUnity.lean

Modified Mathlib/Topology/Order/Bounded.lean

Modified Mathlib/Topology/Semicontinuous.lean

Modified Mathlib/Topology/UnitInterval.lean

Modified MathlibTest/LibrarySearch/IsCompact.lean

Modified MathlibTest/peel.lean