Commit 2024-02-11 18:26 78e6ce74

View on Github →

chore(*): use notation for nhds (#10416) Also fix GeneralizedContinuedFraction.of_convergence: it worked for the Preorder.topology only.

Estimated changes

Modified Mathlib/Algebra/ContinuedFractions/Computation/ApproximationCorollaries.lean

modified theorem GeneralizedContinuedFraction.of_convergence

Modified Mathlib/Analysis/Convex/Body.lean

Modified Mathlib/Analysis/InnerProductSpace/Projection.lean

Modified Mathlib/Analysis/LocallyConvex/WithSeminorms.lean

Modified Mathlib/Analysis/SpecialFunctions/Pow/Asymptotics.lean

Modified Mathlib/Analysis/SpecialFunctions/Pow/Deriv.lean

Modified Mathlib/Analysis/SpecificLimits/Basic.lean

Modified Mathlib/Analysis/SpecificLimits/IsROrC.lean

Modified Mathlib/Analysis/SpecificLimits/Normed.lean

Modified Mathlib/Geometry/Manifold/IntegralCurve.lean

Modified Mathlib/Geometry/Manifold/InteriorBoundary.lean

Modified Mathlib/MeasureTheory/Function/AEEqOfIntegral.lean

Modified Mathlib/MeasureTheory/Function/LpSpace.lean

Modified Mathlib/NumberTheory/SumPrimeReciprocals.lean

Modified Mathlib/Topology/Algebra/Nonarchimedean/Basic.lean

modified theorem NonarchimedeanGroup.prod_self_subset

modified theorem NonarchimedeanGroup.prod_subset

Modified Mathlib/Topology/Category/Stonean/Basic.lean

Modified Mathlib/Topology/Compactness/Lindelof.lean

Modified Mathlib/Topology/ContinuousFunction/Basic.lean

Modified Mathlib/Topology/ContinuousOn.lean

Modified Mathlib/Topology/Instances/TrivSqZeroExt.lean

modified theorem TrivSqZeroExt.nhds_def

modified theorem TrivSqZeroExt.nhds_inl

modified theorem TrivSqZeroExt.nhds_inr

Modified Mathlib/Topology/MetricSpace/PseudoMetric.lean