Commit 2026-11-10 14:11 6b3a071e

View on Github →

chore: golf using finiteness (#45749)

Estimated changes

Modified Mathlib/Analysis/BoundedVariation.lean

Modified Mathlib/Analysis/Distribution/SchwartzSpace/Basic.lean

Modified Mathlib/MeasureTheory/Function/ConditionalExpectation/CondexpL2.lean

Modified Mathlib/MeasureTheory/Function/L1Space/Integrable.lean

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

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

Modified Mathlib/MeasureTheory/Function/SimpleFuncDenseLp.lean

Modified Mathlib/MeasureTheory/Integral/BoundedContinuousFunction.lean

Modified Mathlib/MeasureTheory/Integral/Lebesgue/Countable.lean

Modified Mathlib/MeasureTheory/Integral/Prod.lean

Modified Mathlib/MeasureTheory/Integral/SetToL1/ChangeMeasure.lean

Modified Mathlib/MeasureTheory/Measure/Hausdorff.lean

Modified Mathlib/MeasureTheory/Measure/Prod.lean

Modified Mathlib/MeasureTheory/Measure/Typeclasses/SFinite.lean

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

Modified Mathlib/Topology/MetricSpace/Antilipschitz.lean