Commit 2025-01-31 16:21 2993934d

View on Github →

feat(ENNReal/Basic): add ofNat_ne_top and top_ne_ofNat (#14486) Also deprecate two_ne_top and two_lt_top.

Estimated changes

Modified Mathlib/Analysis/InnerProductSpace/l2Space.lean

Modified Mathlib/Analysis/Matrix.lean

Modified Mathlib/Analysis/MeanInequalitiesPow.lean

Modified Mathlib/Data/ENNReal/Basic.lean

added theorem ENNReal.top_ne_ofNat

modified theorem ENNReal.two_lt_top

modified theorem ENNReal.two_ne_top

Modified Mathlib/Data/ENNReal/Inv.lean

modified theorem ENNReal.inv_three_add_inv_three

Modified Mathlib/MeasureTheory/Covering/Besicovitch.lean

Modified Mathlib/MeasureTheory/Function/ConvergenceInMeasure.lean

Modified Mathlib/MeasureTheory/Function/L2Space.lean

Modified Mathlib/MeasureTheory/Function/LpSeminorm/TriangleInequality.lean

Modified Mathlib/MeasureTheory/Group/GeometryOfNumbers.lean

Modified Mathlib/MeasureTheory/Integral/Bochner.lean

Modified Mathlib/MeasureTheory/Integral/MeanInequalities.lean

Modified Mathlib/MeasureTheory/Measure/LevyProkhorovMetric.lean

Modified Mathlib/NumberTheory/NumberField/CanonicalEmbedding/ConvexBody.lean

Modified Mathlib/Probability/Variance.lean

Modified Mathlib/Topology/EMetricSpace/Defs.lean

Modified Mathlib/Topology/EMetricSpace/Paracompact.lean

Modified Mathlib/Topology/Instances/ENNReal/Lemmas.lean