Commit 2023-05-15 10:07 9ec7de3c

View on Github →

chore: tidy various files (#3996)

Estimated changes

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

Modified Mathlib/Analysis/NormedSpace/CompactOperator.lean

added theorem IsCompactOperator.image_subset_compact_of_isVonNBounded

deleted theorem IsCompactOperator.image_subset_compact_of_vonN_bounded

added theorem IsCompactOperator.isCompact_closure_image_of_isVonNBounded

deleted theorem IsCompactOperator.isCompact_closure_image_of_vonN_bounded

Modified Mathlib/Analysis/SpecificLimits/Basic.lean

Modified Mathlib/CategoryTheory/Functor/LeftDerived.lean

Modified Mathlib/CategoryTheory/Preadditive/InjectiveResolution.lean

Modified Mathlib/CategoryTheory/Subobject/Basic.lean

Modified Mathlib/Data/Complex/Exponential.lean

Modified Mathlib/Data/Num/Lemmas.lean

Modified Mathlib/Data/Real/ENNReal.lean

Modified Mathlib/LinearAlgebra/ProjectiveSpace/Subspace.lean

Modified Mathlib/MeasureTheory/Measure/Sub.lean

Modified Mathlib/NumberTheory/LucasLehmer.lean

Modified Mathlib/Order/KrullDimension.lean

Modified Mathlib/Topology/Category/Profinite/AsLimit.lean

Modified Mathlib/Topology/ContinuousFunction/Algebra.lean

Modified Mathlib/Topology/MetricSpace/Basic.lean

added theorem Metric.tendsto_atTop'

deleted theorem Metric.tendsto_at_top'