Commit 2025-04-04 03:49 efac006f

View on Github →

chore: split Topology.ContinuousMap.Bounded.Basic (#23574) Split off

Topology.ContinuousMap.Bounded.Normed, showing that normed algebraic structures can be inherited by bounded continuous functions
Topology.ContinuousMap.Bounded.ArzelaAscoli, containing the Arzelà–Ascoli theorem

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Analysis/Normed/Lp/LpEquiv.lean

Modified Mathlib/Analysis/SpecialFunctions/MulExpNegMulSq.lean

Modified Mathlib/MeasureTheory/Integral/BoundedContinuousFunction.lean

Created Mathlib/Topology/ContinuousMap/Bounded/ArzelaAscoli.lean

added theorem BoundedContinuousFunction.arzela_ascoli

added theorem BoundedContinuousFunction.arzela_ascoli₁

added theorem BoundedContinuousFunction.arzela_ascoli₂

Modified Mathlib/Topology/ContinuousMap/Bounded/Basic.lean

deleted def BoundedContinuousFunction.C

deleted theorem BoundedContinuousFunction.abs_diff_coe_le_dist

deleted theorem BoundedContinuousFunction.abs_self_eq_nnrealPart_add_nnrealPart_neg

deleted theorem BoundedContinuousFunction.add_norm_nonneg

deleted theorem BoundedContinuousFunction.algebraMap_apply

deleted theorem BoundedContinuousFunction.apply_le_norm

deleted theorem BoundedContinuousFunction.arzela_ascoli

deleted theorem BoundedContinuousFunction.arzela_ascoli₁

deleted theorem BoundedContinuousFunction.arzela_ascoli₂

deleted theorem BoundedContinuousFunction.bddAbove_range_norm_comp

deleted theorem BoundedContinuousFunction.coe_abs

deleted theorem BoundedContinuousFunction.coe_inf

deleted theorem BoundedContinuousFunction.coe_intCast

deleted theorem BoundedContinuousFunction.coe_le_coe_add_dist

deleted theorem BoundedContinuousFunction.coe_natCast

deleted theorem BoundedContinuousFunction.coe_neg

deleted theorem BoundedContinuousFunction.coe_negPart

deleted theorem BoundedContinuousFunction.coe_normComp

deleted theorem BoundedContinuousFunction.coe_npowRec

deleted theorem BoundedContinuousFunction.coe_ofNat

deleted theorem BoundedContinuousFunction.coe_ofNormedAddCommGroup

deleted theorem BoundedContinuousFunction.coe_ofNormedAddCommGroupDiscrete

deleted theorem BoundedContinuousFunction.coe_posPart

deleted theorem BoundedContinuousFunction.coe_sup

deleted theorem BoundedContinuousFunction.coe_toContinuousMapₐ

deleted theorem BoundedContinuousFunction.coe_zsmul

deleted theorem BoundedContinuousFunction.coe_zsmulRec

deleted theorem BoundedContinuousFunction.dist_le_two_norm'

deleted theorem BoundedContinuousFunction.dist_le_two_norm

deleted theorem BoundedContinuousFunction.mkOfCompact_neg

deleted theorem BoundedContinuousFunction.mkOfCompact_sub

deleted theorem BoundedContinuousFunction.neg_apply

deleted theorem BoundedContinuousFunction.neg_norm_le_apply

deleted theorem BoundedContinuousFunction.nndist_le_two_nnnorm

deleted def BoundedContinuousFunction.nnnorm

deleted theorem BoundedContinuousFunction.nnnorm_coeFn_eq

deleted theorem BoundedContinuousFunction.nnnorm_coe_le_nnnorm

deleted theorem BoundedContinuousFunction.nnnorm_const_eq

deleted theorem BoundedContinuousFunction.nnnorm_const_le

deleted theorem BoundedContinuousFunction.nnnorm_def

deleted theorem BoundedContinuousFunction.nnnorm_eq_iSup_nnnorm

deleted theorem BoundedContinuousFunction.nnnorm_le

deleted def BoundedContinuousFunction.nnrealPart

deleted theorem BoundedContinuousFunction.nnrealPart_coeFn_eq

deleted def BoundedContinuousFunction.normComp

deleted theorem BoundedContinuousFunction.norm_coe_le_norm

deleted theorem BoundedContinuousFunction.norm_compContinuous_le

deleted theorem BoundedContinuousFunction.norm_const_eq

deleted theorem BoundedContinuousFunction.norm_const_le

deleted theorem BoundedContinuousFunction.norm_def

deleted theorem BoundedContinuousFunction.norm_eq

deleted theorem BoundedContinuousFunction.norm_eq_iSup_norm

deleted theorem BoundedContinuousFunction.norm_eq_of_nonempty

deleted theorem BoundedContinuousFunction.norm_eq_zero_of_empty

deleted theorem BoundedContinuousFunction.norm_le

deleted theorem BoundedContinuousFunction.norm_le_of_nonempty

deleted theorem BoundedContinuousFunction.norm_lt_iff_of_compact

deleted theorem BoundedContinuousFunction.norm_lt_iff_of_nonempty_compact

deleted theorem BoundedContinuousFunction.norm_normComp

deleted theorem BoundedContinuousFunction.norm_ofNormedAddCommGroup_le

deleted theorem BoundedContinuousFunction.norm_sub_nonneg

deleted def BoundedContinuousFunction.ofNormedAddCommGroup

deleted def BoundedContinuousFunction.ofNormedAddCommGroupDiscrete

deleted theorem BoundedContinuousFunction.self_eq_nnrealPart_sub_nnrealPart_neg

deleted def BoundedContinuousFunction.toContinuousMapₐ

deleted theorem BoundedContinuousFunction.zsmul_apply

deleted theorem ContinuousLinearMap.compLeftContinuousBounded_apply

Created Mathlib/Topology/ContinuousMap/Bounded/Normed.lean

added def BoundedContinuousFunction.C

added theorem BoundedContinuousFunction.abs_diff_coe_le_dist

added theorem BoundedContinuousFunction.abs_self_eq_nnrealPart_add_nnrealPart_neg

added theorem BoundedContinuousFunction.add_norm_nonneg

added theorem BoundedContinuousFunction.algebraMap_apply

added theorem BoundedContinuousFunction.apply_le_norm

added theorem BoundedContinuousFunction.bddAbove_range_norm_comp

added theorem BoundedContinuousFunction.coe_abs

added theorem BoundedContinuousFunction.coe_inf

added theorem BoundedContinuousFunction.coe_intCast

added theorem BoundedContinuousFunction.coe_le_coe_add_dist

added theorem BoundedContinuousFunction.coe_natCast

added theorem BoundedContinuousFunction.coe_neg

added theorem BoundedContinuousFunction.coe_negPart

added theorem BoundedContinuousFunction.coe_normComp

added theorem BoundedContinuousFunction.coe_npowRec

added theorem BoundedContinuousFunction.coe_ofNat

added theorem BoundedContinuousFunction.coe_ofNormedAddCommGroup

added theorem BoundedContinuousFunction.coe_ofNormedAddCommGroupDiscrete

added theorem BoundedContinuousFunction.coe_posPart

added theorem BoundedContinuousFunction.coe_sup

added theorem BoundedContinuousFunction.coe_toContinuousMapₐ

added theorem BoundedContinuousFunction.coe_zsmul

added theorem BoundedContinuousFunction.coe_zsmulRec

added theorem BoundedContinuousFunction.dist_le_two_norm'

added theorem BoundedContinuousFunction.dist_le_two_norm

added theorem BoundedContinuousFunction.mkOfCompact_neg

added theorem BoundedContinuousFunction.mkOfCompact_sub

added theorem BoundedContinuousFunction.neg_apply

added theorem BoundedContinuousFunction.neg_norm_le_apply

added theorem BoundedContinuousFunction.nndist_le_two_nnnorm

added def BoundedContinuousFunction.nnnorm

added theorem BoundedContinuousFunction.nnnorm_coeFn_eq

added theorem BoundedContinuousFunction.nnnorm_coe_le_nnnorm

added theorem BoundedContinuousFunction.nnnorm_const_eq

added theorem BoundedContinuousFunction.nnnorm_const_le

added theorem BoundedContinuousFunction.nnnorm_def

added theorem BoundedContinuousFunction.nnnorm_eq_iSup_nnnorm

added theorem BoundedContinuousFunction.nnnorm_le

added def BoundedContinuousFunction.nnrealPart

added theorem BoundedContinuousFunction.nnrealPart_coeFn_eq

added def BoundedContinuousFunction.normComp

added theorem BoundedContinuousFunction.norm_coe_le_norm

added theorem BoundedContinuousFunction.norm_compContinuous_le

added theorem BoundedContinuousFunction.norm_const_eq

added theorem BoundedContinuousFunction.norm_const_le

added theorem BoundedContinuousFunction.norm_def

added theorem BoundedContinuousFunction.norm_eq

added theorem BoundedContinuousFunction.norm_eq_iSup_norm

added theorem BoundedContinuousFunction.norm_eq_of_nonempty

added theorem BoundedContinuousFunction.norm_eq_zero_of_empty

added theorem BoundedContinuousFunction.norm_le

added theorem BoundedContinuousFunction.norm_le_of_nonempty

added theorem BoundedContinuousFunction.norm_lt_iff_of_compact

added theorem BoundedContinuousFunction.norm_lt_iff_of_nonempty_compact

added theorem BoundedContinuousFunction.norm_normComp

added theorem BoundedContinuousFunction.norm_ofNormedAddCommGroup_le

added theorem BoundedContinuousFunction.norm_sub_nonneg

added def BoundedContinuousFunction.ofNormedAddCommGroup

added def BoundedContinuousFunction.ofNormedAddCommGroupDiscrete

added theorem BoundedContinuousFunction.self_eq_nnrealPart_sub_nnrealPart_neg

added def BoundedContinuousFunction.toContinuousMapₐ

added theorem BoundedContinuousFunction.zsmul_apply

added theorem ContinuousLinearMap.compLeftContinuousBounded_apply

Modified Mathlib/Topology/ContinuousMap/Bounded/Star.lean

Modified Mathlib/Topology/ContinuousMap/BoundedCompactlySupported.lean

Modified Mathlib/Topology/MetricSpace/GromovHausdorffRealized.lean

Modified Mathlib/Topology/TietzeExtension.lean