Commit 2023-09-19 04:03 98e78f90

View on Github →

refactor(Topology/MetricSpace): remove Metric.Bounded (#7240) Use Bornology.IsBounded instead.

Estimated changes

Modified Mathlib/Algebra/Module/Zlattice.lean

deleted theorem Zspan.fundamentalDomain_bounded

added theorem Zspan.fundamentalDomain_isBounded

Modified Mathlib/Analysis/BoxIntegral/DivergenceTheorem.lean

Modified Mathlib/Analysis/BoxIntegral/Partition/Tagged.lean

Modified Mathlib/Analysis/Calculus/BumpFunction/FiniteDimension.lean

Modified Mathlib/Analysis/Complex/AbsMax.lean

modified theorem Complex.eqOn_closure_of_eqOn_frontier

modified theorem Complex.eqOn_of_eqOn_frontier

modified theorem Complex.norm_le_of_forall_mem_frontier_norm_le

Modified Mathlib/Analysis/Complex/Liouville.lean

modified theorem Complex.liouville_theorem_aux

modified theorem Differentiable.apply_eq_apply_of_bounded

modified theorem Differentiable.exists_eq_const_of_bounded

Modified Mathlib/Analysis/Complex/PhragmenLindelof.lean

Modified Mathlib/Analysis/Complex/Polynomial.lean

Modified Mathlib/Analysis/Complex/ReImTopology.lean

added theorem Bornology.IsBounded.reProdIm

deleted theorem Metric.Bounded.reProdIm

Modified Mathlib/Analysis/Complex/Schwarz.lean

Modified Mathlib/Analysis/Convex/Body.lean

Modified Mathlib/Analysis/Convex/Measure.lean

Modified Mathlib/Analysis/Convex/Normed.lean

deleted theorem bounded_convexHull

added theorem isBounded_convexHull

Modified Mathlib/Analysis/Convex/Topology.lean

modified theorem bounded_stdSimplex

modified theorem stdSimplex_subset_closedBall

Modified Mathlib/Analysis/Convolution.lean

Modified Mathlib/Analysis/Fourier/PoissonSummation.lean

Modified Mathlib/Analysis/InnerProductSpace/MeanErgodic.lean

Modified Mathlib/Analysis/LocallyConvex/Bounded.lean

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

added theorem Bornology.IsBounded.exists_pos_norm_le'

deleted theorem Metric.Bounded.exists_pos_norm_le'

deleted theorem bounded_iff_forall_norm_le'

added theorem isBounded_iff_forall_norm_le'

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

added theorem Bornology.IsBounded.div

added theorem Bornology.IsBounded.inv

added theorem Bornology.IsBounded.mul

deleted theorem Metric.Bounded.div

deleted theorem Metric.Bounded.inv

deleted theorem Metric.Bounded.mul

Modified Mathlib/Analysis/NormedSpace/Basic.lean

Modified Mathlib/Analysis/NormedSpace/CompactOperator.lean

Modified Mathlib/Analysis/NormedSpace/Dual.lean

deleted theorem NormedSpace.bounded_polar_of_mem_nhds_zero

added theorem NormedSpace.isBounded_polar_of_mem_nhds_zero

Modified Mathlib/Analysis/NormedSpace/OperatorNorm.lean

modified theorem ContinuousLinearMap.isClosed_image_coe_of_bounded_of_weak_closed

modified def ContinuousLinearMap.ofMemClosureImageCoeBounded

Modified Mathlib/Analysis/NormedSpace/Pointwise.lean

added theorem Bornology.IsBounded.smul₀

deleted theorem Metric.Bounded.smul₀

modified theorem eventually_singleton_add_smul_subset

Modified Mathlib/Analysis/NormedSpace/Spectrum.lean

added theorem spectrum.isBounded

deleted theorem spectrum.is_bounded

Modified Mathlib/Analysis/NormedSpace/WeakDual.lean

Modified Mathlib/Analysis/NormedSpace/lpSpace.lean

modified theorem lp.memℓp_of_tendsto

Modified Mathlib/Data/Set/Image.lean

Modified Mathlib/Dynamics/BirkhoffSum/NormedSpace.lean

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

Modified Mathlib/MeasureTheory/Constructions/Polish.lean

Modified Mathlib/MeasureTheory/Function/ContinuousMapDense.lean

Modified Mathlib/MeasureTheory/Function/Jacobian.lean

Modified Mathlib/MeasureTheory/Function/LocallyIntegrable.lean

Modified Mathlib/MeasureTheory/Measure/Lebesgue/Basic.lean

Modified Mathlib/MeasureTheory/Measure/Lebesgue/EqHaar.lean

Modified Mathlib/MeasureTheory/Measure/MeasureSpace.lean

added theorem Bornology.IsBounded.measure_lt_top

deleted theorem Metric.Bounded.measure_lt_top

Modified Mathlib/Topology/Bornology/Basic.lean

added theorem Bornology.IsBounded.insert

modified def Bornology.cofinite

added theorem Bornology.isBounded_iff_forall_mem

added theorem Bornology.isBounded_insert

added theorem Filter.HasBasis.disjoint_cobounded_iff

Modified Mathlib/Topology/Bornology/Hom.lean

added theorem Bornology.IsBounded.image

deleted theorem IsBounded.image

Modified Mathlib/Topology/ContinuousFunction/Bounded.lean

deleted theorem BoundedContinuousFunction.bounded_image

deleted theorem BoundedContinuousFunction.bounded_range

added theorem BoundedContinuousFunction.isBounded_image

added theorem BoundedContinuousFunction.isBounded_range

Modified Mathlib/Topology/ContinuousFunction/ZeroAtInfty.lean

deleted theorem ZeroAtInftyContinuousMap.bounded_image

deleted theorem ZeroAtInftyContinuousMap.bounded_range

added theorem ZeroAtInftyContinuousMap.isBounded_image

added theorem ZeroAtInftyContinuousMap.isBounded_range

Modified Mathlib/Topology/Instances/ENNReal.lean

modified theorem Real.diam_eq

modified theorem Real.ediam_eq

Modified Mathlib/Topology/Instances/Real.lean

deleted theorem Function.Periodic.bounded_of_continuous

added theorem Function.Periodic.isBounded_of_continuous

deleted theorem Real.bounded_iff_bddBelow_bddAbove

added theorem Real.isBounded_iff_bddBelow_bddAbove

deleted theorem Real.subset_Icc_sInf_sSup_of_bounded

added theorem Real.subset_Icc_sInf_sSup_of_isBounded

Modified Mathlib/Topology/MetricSpace/Antilipschitz.lean

deleted theorem AntilipschitzWith.bounded_preimage

added theorem AntilipschitzWith.isBounded_preimage

Modified Mathlib/Topology/MetricSpace/Basic.lean

added theorem Bornology.IsBounded.isCompact_closure

added theorem Bornology.IsBounded.subset_ball

added theorem Bornology.IsBounded.subset_ball_lt

added theorem Bornology.IsBounded.subset_closedBall

added theorem Bornology.IsBounded.subset_closedBall_lt

deleted theorem CauchySeq.bounded_range

added theorem CauchySeq.isBounded_range

modified theorem Filter.Tendsto.congr_dist

deleted theorem IsCompact.bounded

added theorem IsCompact.isBounded

deleted theorem Metric.Bounded.ediam_ne_top

deleted theorem Metric.Bounded.isCompact_closure

deleted theorem Metric.Bounded.mono

deleted theorem Metric.Bounded.subset_ball

deleted theorem Metric.Bounded.subset_ball_lt

deleted theorem Metric.Bounded.union

deleted def Metric.Bounded

deleted theorem Metric.Finite_bounded_inter_isClosed

deleted theorem Metric.bounded_Icc

deleted theorem Metric.bounded_Ico

deleted theorem Metric.bounded_Ioc

deleted theorem Metric.bounded_Ioo

deleted theorem Metric.bounded_ball

deleted theorem Metric.bounded_biUnion

deleted theorem Metric.bounded_closedBall

deleted theorem Metric.bounded_closure_iff

deleted theorem Metric.bounded_closure_of_bounded

deleted theorem Metric.bounded_empty

deleted theorem Metric.bounded_iff_ediam_ne_top

deleted theorem Metric.bounded_iff_isBounded

deleted theorem Metric.bounded_iff_mem_bounded

deleted theorem Metric.bounded_iff_subset_ball

deleted theorem Metric.bounded_of_bddAbove_of_bddBelow

deleted theorem Metric.bounded_of_compactSpace

deleted theorem Metric.bounded_of_finite

deleted theorem Metric.bounded_range_iff

deleted theorem Metric.bounded_range_of_cauchy_map_cofinite

deleted theorem Metric.bounded_range_of_tendsto

deleted theorem Metric.bounded_range_of_tendsto_cofinite

deleted theorem Metric.bounded_range_of_tendsto_cofinite_uniformity

deleted theorem Metric.bounded_singleton

deleted theorem Metric.bounded_sphere

deleted theorem Metric.bounded_union

deleted theorem Metric.compactSpace_iff_bounded_univ

added theorem Metric.compactSpace_iff_isBounded_univ

modified theorem Metric.diam_eq_zero_of_unbounded

modified theorem Metric.diam_mono

added theorem Metric.disjoint_cobounded_nhds

added theorem Metric.disjoint_cobounded_nhdsSet

added theorem Metric.disjoint_nhdsSet_cobounded

added theorem Metric.disjoint_nhds_cobounded

modified theorem Metric.dist_le_diam_of_mem

modified theorem Metric.ediam_eq_top_iff_unbounded

modified theorem Metric.ediam_of_unbounded

modified theorem Metric.eventually_nhds_prod_iff

deleted theorem Metric.exists_isOpen_bounded_image_inter_of_isCompact_of_continuousOn

deleted theorem Metric.exists_isOpen_bounded_image_inter_of_isCompact_of_forall_continuousWithinAt

deleted theorem Metric.exists_isOpen_bounded_image_of_isCompact_of_continuousOn

deleted theorem Metric.exists_isOpen_bounded_image_of_isCompact_of_forall_continuousAt

added theorem Metric.exists_isOpen_isBounded_image_inter_of_isCompact_of_continuousOn

added theorem Metric.exists_isOpen_isBounded_image_inter_of_isCompact_of_forall_continuousWithinAt

added theorem Metric.exists_isOpen_isBounded_image_of_isCompact_of_continuousOn

added theorem Metric.exists_isOpen_isBounded_image_of_isCompact_of_forall_continuousAt

added theorem Metric.finite_isBounded_inter_isClosed

added theorem Metric.isBounded_Icc

added theorem Metric.isBounded_Ico

added theorem Metric.isBounded_Ioc

added theorem Metric.isBounded_Ioo

added theorem Metric.isBounded_ball

added theorem Metric.isBounded_closedBall

added theorem Metric.isBounded_closure_iff

added theorem Metric.isBounded_closure_of_isBounded

added theorem Metric.isBounded_iff_ediam_ne_top

added theorem Metric.isBounded_iff_subset_closedBall

added theorem Metric.isBounded_image_iff

added theorem Metric.isBounded_of_bddAbove_of_bddBelow

added theorem Metric.isBounded_of_compactSpace

added theorem Metric.isBounded_range_iff

added theorem Metric.isBounded_range_of_cauchy_map_cofinite

added theorem Metric.isBounded_range_of_tendsto

added theorem Metric.isBounded_range_of_tendsto_cofinite

added theorem Metric.isBounded_range_of_tendsto_cofinite_uniformity

added theorem Metric.isBounded_sphere

deleted theorem Metric.isCompact_of_isClosed_bounded

added theorem Metric.isCompact_of_isClosed_isBounded

modified theorem Metric.tendstoLocallyUniformlyOn_iff

modified theorem Metric.tendstoLocallyUniformly_iff

modified theorem Metric.tendstoUniformlyOnFilter_iff

modified theorem Metric.tendstoUniformlyOn_iff

modified theorem Metric.tendstoUniformly_iff

deleted theorem TotallyBounded.bounded

added theorem TotallyBounded.isBounded

modified theorem lebesgue_number_lemma_of_metric

modified theorem tendsto_iff_of_dist

modified theorem tendsto_uniformity_iff_dist_tendsto_zero

Modified Mathlib/Topology/MetricSpace/Closeds.lean

Modified Mathlib/Topology/MetricSpace/GromovHausdorff.lean

Modified Mathlib/Topology/MetricSpace/GromovHausdorffRealized.lean

Modified Mathlib/Topology/MetricSpace/HausdorffDistance.lean

added theorem Bornology.IsBounded.cthickening

deleted theorem Metric.Bounded.cthickening

modified theorem Metric.dist_le_infDist_add_diam

modified theorem Metric.hausdorffDist_le_diam

Modified Mathlib/Topology/MetricSpace/IsometricSMul.lean

added theorem Bornology.IsBounded.smul

deleted theorem Metric.Bounded.smul

Modified Mathlib/Topology/MetricSpace/Lipschitz.lean

deleted theorem LipschitzWith.bounded_image

modified theorem LipschitzWith.diam_image_le

added theorem LipschitzWith.isBounded_image

deleted theorem Metric.Bounded.left_of_prod

deleted theorem Metric.Bounded.right_of_prod

deleted theorem Metric.bounded_prod

deleted theorem Metric.bounded_prod_of_nonempty

Modified Mathlib/Topology/MetricSpace/PiNat.lean

Modified Mathlib/Topology/Sequences.lean

modified theorem tendsto_subseq_of_bounded

modified theorem tendsto_subseq_of_frequently_bounded

Modified Mathlib/Topology/TietzeExtension.lean