Commit 2023-05-25 08:46 74e10fe8

View on Github →

feat: port Topology.ContinuousFunction.Compact (#4183)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Topology/ContinuousFunction/Compact.lean

added theorem BoundedContinuousFunction.dist_mkOfCompact

added theorem BoundedContinuousFunction.dist_toContinuousMap

added theorem BoundedContinuousFunction.mkOfCompact_star

added theorem BoundedContinuousFunction.norm_mkOfCompact

added theorem BoundedContinuousFunction.norm_toContinuousMap_eq

added theorem ContinuousLinearMap.compLeftContinuousCompact_apply

added theorem ContinuousLinearMap.toLinear_compLeftContinuousCompact

added def ContinuousMap.addEquivBoundedOfCompact

added theorem ContinuousMap.addEquivBoundedOfCompact_apply

added theorem ContinuousMap.addEquivBoundedOfCompact_symm_apply

added theorem ContinuousMap.apply_le_norm

added theorem ContinuousMap.compRightAlgHom_continuous

added def ContinuousMap.compRightContinuousMap

added theorem ContinuousMap.compRightContinuousMap_apply

added def ContinuousMap.compRightHomeomorph

added theorem ContinuousMap.continuous_coe

added theorem ContinuousMap.continuous_eval

added theorem ContinuousMap.continuous_eval_const

added theorem ContinuousMap.dist_apply_le_dist

added theorem ContinuousMap.dist_le

added theorem ContinuousMap.dist_le_iff_of_nonempty

added theorem ContinuousMap.dist_le_two_norm

added theorem ContinuousMap.dist_lt_iff

added theorem ContinuousMap.dist_lt_iff_of_nonempty

added theorem ContinuousMap.dist_lt_of_dist_lt_modulus

added theorem ContinuousMap.dist_lt_of_nonempty

added def ContinuousMap.equivBoundedOfCompact

added def ContinuousMap.evalClm

added def ContinuousMap.isometryEquivBoundedOfCompact

added def ContinuousMap.linearIsometryBoundedOfCompact

added theorem ContinuousMap.linearIsometryBoundedOfCompact_apply_apply

added theorem ContinuousMap.linearIsometryBoundedOfCompact_of_compact_toEquiv

added theorem ContinuousMap.linearIsometryBoundedOfCompact_symm_apply

added theorem ContinuousMap.linearIsometryBoundedOfCompact_toAddEquiv

added theorem ContinuousMap.linearIsometryBoundedOfCompact_toIsometryEquiv

added def ContinuousMap.modulus

added theorem ContinuousMap.modulus_pos

added theorem ContinuousMap.neg_norm_le_apply

added theorem ContinuousMap.nnnorm_lt_iff

added theorem ContinuousMap.nnnorm_lt_iff_of_nonempty

added theorem ContinuousMap.norm_coe_le_norm

added theorem ContinuousMap.norm_eq_iSup_norm

added theorem ContinuousMap.norm_le

added theorem ContinuousMap.norm_le_of_nonempty

added theorem ContinuousMap.norm_lt_iff

added theorem ContinuousMap.norm_lt_iff_of_nonempty

added theorem ContinuousMap.norm_restrict_mono_set

added theorem ContinuousMap.summable_of_locally_summable_norm

added theorem ContinuousMap.uniformEmbedding_equivBoundedOfCompact

added theorem ContinuousMap.uniformInducing_equivBoundedOfCompact

added theorem ContinuousMap.uniform_continuity