Commit 2023-11-08 15:51 11572f18

View on Github →

chore: tidy various files (#8175)

Estimated changes

Modified Archive/Imo/Imo2005Q4.lean

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

Modified Mathlib/Analysis/Normed/Group/SemiNormedGroupCat/Completion.lean

Modified Mathlib/Data/List/Lex.lean

Modified Mathlib/Data/Set/Function.lean

added theorem Set.eqOn_univ

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

added theorem measurable_of_isClosed'

deleted theorem measurable_of_is_closed'

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

Modified Mathlib/MeasureTheory/Measure/MeasureSpace.lean

Modified Mathlib/NumberTheory/ArithmeticFunction.lean

Modified Mathlib/Order/Filter/AtTopBot.lean

Modified Mathlib/RingTheory/HahnSeries.lean

modified theorem HahnSeries.single_eq_zero_iff

Modified Mathlib/RingTheory/PowerSeries/Derivative.lean

Modified Mathlib/Topology/Connected/PathConnected.lean

Modified Mathlib/Topology/MetricSpace/Basic.lean

Modified Mathlib/Topology/MetricSpace/Bounded.lean

Modified Mathlib/Topology/MetricSpace/Cauchy.lean

Modified Mathlib/Topology/MetricSpace/PseudoMetric.lean

Modified Mathlib/Topology/Sheaves/Functors.lean

Modified Mathlib/Topology/Sheaves/SheafCondition/Sites.lean