Commit 2024-10-18 09:18 8e0ebee2

View on Github →

chore(*): fix some TODOs (#17891) Also drop an unneeded assumption in a lemma.

Estimated changes

Modified Mathlib/Algebra/Order/Monoid/Unbundled/ExistsOfLE.lean

modified theorem le_iff_forall_one_lt_lt_mul'

Modified Mathlib/Analysis/Calculus/ContDiff/Basic.lean

Modified Mathlib/Analysis/Oscillation.lean

Modified Mathlib/Data/Finset/Card.lean

Modified Mathlib/Data/NNReal/Basic.lean

Modified Mathlib/MeasureTheory/Integral/RieszMarkovKakutani.lean

Modified Mathlib/Topology/MetricSpace/HausdorffDistance.lean