Commit 2023-05-21 21:51 5e4ff038

View on Github →

feat: port Topology.ContinuousFunction.Bounded (#4075)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Topology/ContinuousFunction/Bounded.lean

added def BoundedContinuousFunction.C

added theorem BoundedContinuousFunction.Nnreal.upper_bound

added def BoundedContinuousFunction.Simps.apply

added theorem BoundedContinuousFunction.abs_diff_coe_le_dist

added theorem BoundedContinuousFunction.abs_self_eq_nnrealPart_add_nnrealPart_neg

added theorem BoundedContinuousFunction.add_apply

added theorem BoundedContinuousFunction.add_compContinuous

added theorem BoundedContinuousFunction.algebraMap_apply

added theorem BoundedContinuousFunction.arzela_ascoli

added theorem BoundedContinuousFunction.arzela_ascoli₁

added theorem BoundedContinuousFunction.arzela_ascoli₂

added theorem BoundedContinuousFunction.bddAbove_range_norm_comp

added theorem BoundedContinuousFunction.bounded_image

added theorem BoundedContinuousFunction.bounded_range

added def BoundedContinuousFunction.codRestrict

added def BoundedContinuousFunction.coeFnAddHom

added theorem BoundedContinuousFunction.coeFn_abs

added theorem BoundedContinuousFunction.coeFn_sup

added theorem BoundedContinuousFunction.coe_add

added theorem BoundedContinuousFunction.coe_compContinuous

added theorem BoundedContinuousFunction.coe_intCast

added theorem BoundedContinuousFunction.coe_le_coe_add_dist

added theorem BoundedContinuousFunction.coe_mul

added theorem BoundedContinuousFunction.coe_natCast

added theorem BoundedContinuousFunction.coe_neg

added theorem BoundedContinuousFunction.coe_normComp

added theorem BoundedContinuousFunction.coe_npowRec

added theorem BoundedContinuousFunction.coe_nsmul

added theorem BoundedContinuousFunction.coe_nsmulRec

added theorem BoundedContinuousFunction.coe_ofNormedAddCommGroup

added theorem BoundedContinuousFunction.coe_ofNormedAddCommGroupDiscrete

added theorem BoundedContinuousFunction.coe_one

added theorem BoundedContinuousFunction.coe_pow

added theorem BoundedContinuousFunction.coe_restrict

added theorem BoundedContinuousFunction.coe_smul

added theorem BoundedContinuousFunction.coe_star

added theorem BoundedContinuousFunction.coe_sub

added theorem BoundedContinuousFunction.coe_sum

added theorem BoundedContinuousFunction.coe_to_continuous_fun

added theorem BoundedContinuousFunction.coe_zsmul

added theorem BoundedContinuousFunction.coe_zsmulRec

added def BoundedContinuousFunction.comp

added def BoundedContinuousFunction.compContinuous

added theorem BoundedContinuousFunction.compContinuous_apply

added def BoundedContinuousFunction.const

added theorem BoundedContinuousFunction.const_apply'

added theorem BoundedContinuousFunction.continuous_coe

added theorem BoundedContinuousFunction.continuous_comp

added theorem BoundedContinuousFunction.continuous_compContinuous

added theorem BoundedContinuousFunction.continuous_eval

added theorem BoundedContinuousFunction.continuous_eval_const

added theorem BoundedContinuousFunction.dist_coe_le_dist

added theorem BoundedContinuousFunction.dist_eq

added theorem BoundedContinuousFunction.dist_eq_iSup

added theorem BoundedContinuousFunction.dist_extend_extend

added theorem BoundedContinuousFunction.dist_le

added theorem BoundedContinuousFunction.dist_le_iff_of_nonempty

added theorem BoundedContinuousFunction.dist_le_two_norm'

added theorem BoundedContinuousFunction.dist_le_two_norm

added theorem BoundedContinuousFunction.dist_lt_iff_of_compact

added theorem BoundedContinuousFunction.dist_lt_iff_of_nonempty_compact

added theorem BoundedContinuousFunction.dist_lt_of_nonempty_compact

added theorem BoundedContinuousFunction.dist_set_exists

added theorem BoundedContinuousFunction.dist_zero_of_empty

added theorem BoundedContinuousFunction.embedding_coeFn

added theorem BoundedContinuousFunction.eq_of_empty

added def BoundedContinuousFunction.evalClm

added theorem BoundedContinuousFunction.evalClm_apply

added theorem BoundedContinuousFunction.ext

added theorem BoundedContinuousFunction.extend_apply

added theorem BoundedContinuousFunction.extend_of_empty

added theorem BoundedContinuousFunction.forall_coe_one_iff_one

added theorem BoundedContinuousFunction.inducing_coeFn

added theorem BoundedContinuousFunction.isometry_extend

added theorem BoundedContinuousFunction.lipschitz_comp

added theorem BoundedContinuousFunction.lipschitz_compContinuous

added theorem BoundedContinuousFunction.lipschitz_evalx

added def BoundedContinuousFunction.mkOfBound

added theorem BoundedContinuousFunction.mkOfBound_coe

added def BoundedContinuousFunction.mkOfCompact

added theorem BoundedContinuousFunction.mkOfCompact_add

added theorem BoundedContinuousFunction.mkOfCompact_apply

added theorem BoundedContinuousFunction.mkOfCompact_neg

added theorem BoundedContinuousFunction.mkOfCompact_one

added theorem BoundedContinuousFunction.mkOfCompact_sub

added def BoundedContinuousFunction.mkOfDiscrete

added theorem BoundedContinuousFunction.mul_apply

added theorem BoundedContinuousFunction.neg_apply

added theorem BoundedContinuousFunction.nndist_coe_le_nndist

added theorem BoundedContinuousFunction.nndist_eq

added theorem BoundedContinuousFunction.nndist_eq_iSup

added theorem BoundedContinuousFunction.nndist_le_two_nnnorm

added theorem BoundedContinuousFunction.nndist_set_exists

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_smul_le

added theorem BoundedContinuousFunction.nsmul_apply

added def BoundedContinuousFunction.ofNormedAddCommGroup

added def BoundedContinuousFunction.ofNormedAddCommGroupDiscrete

added theorem BoundedContinuousFunction.one_compContinuous

added theorem BoundedContinuousFunction.pow_apply

added def BoundedContinuousFunction.restrict

added theorem BoundedContinuousFunction.restrict_apply

added theorem BoundedContinuousFunction.self_eq_nnrealPart_sub_nnrealPart_neg

added theorem BoundedContinuousFunction.smul_apply

added theorem BoundedContinuousFunction.star_apply

added theorem BoundedContinuousFunction.sub_apply

added theorem BoundedContinuousFunction.sum_apply

added theorem BoundedContinuousFunction.tendsto_iff_tendstoUniformly

added def BoundedContinuousFunction.toContinuousMapAddHom

added def BoundedContinuousFunction.toContinuousMapLinearMap

added theorem BoundedContinuousFunction.uniformContinuous_coe

added theorem BoundedContinuousFunction.uniformContinuous_comp

added theorem BoundedContinuousFunction.zsmul_apply

added structure BoundedContinuousFunction

added theorem ContinuousLinearMap.compLeftContinuousBounded_apply