Commit 2024-06-28 09:13 c4dd0246

View on Github →

chore(*): remove some deprecated theorems (#14214)

Estimated changes

Modified Mathlib/Analysis/InnerProductSpace/Calculus.lean

deleted theorem Homeomorph.contDiffOn_unitBall_symm

Modified Mathlib/Logic/Basic.lean

Modified Mathlib/MeasureTheory/MeasurableSpace/Basic.lean

deleted theorem exists_measurable_piecewise_nat

Modified Mathlib/MeasureTheory/MeasurableSpace/Defs.lean

deleted theorem MeasurableSet.biUnion_decode₂

Modified Mathlib/MeasureTheory/Measure/NullMeasurable.lean

Modified Mathlib/NumberTheory/SumFourSquares.lean

deleted theorem Int.exists_sq_add_sq_add_one_eq_k

Modified Mathlib/Topology/Algebra/WithZeroTopology.lean

deleted theorem WithZeroTopology.t3Space

Modified Mathlib/Topology/FiberBundle/Trivialization.lean

deleted theorem Trivialization.open_target'

Modified Mathlib/Topology/Instances/EReal.lean

deleted def EReal.negHomeo

Modified Mathlib/Topology/Instances/Real.lean

deleted theorem Function.Periodic.compact_of_continuous'

deleted theorem Real.Continuous.inv

deleted theorem Real.tendsto_inv