Commit 2023-05-09 23:59 bb9f3620

View on Github →

feat: port Analysis.NormedSpace.CompactOperator (#3805)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Analysis/NormedSpace/CompactOperator.lean

added theorem ContinuousLinearMap.coe_mkOfIsCompactOperator

added def ContinuousLinearMap.mkOfIsCompactOperator

added theorem ContinuousLinearMap.mkOfIsCompactOperator_mem_compactOperator

added theorem ContinuousLinearMap.mkOfIsCompactOperator_to_linearMap

added theorem IsCompactOperator.add

added theorem IsCompactOperator.clm_comp

added theorem IsCompactOperator.codRestrict

added theorem IsCompactOperator.comp_clm

added theorem IsCompactOperator.continuous

added theorem IsCompactOperator.continuous_comp

added theorem IsCompactOperator.image_ball_subset_compact

added theorem IsCompactOperator.image_closedBall_subset_compact

added theorem IsCompactOperator.image_subset_compact_of_bounded

added theorem IsCompactOperator.image_subset_compact_of_vonN_bounded

added theorem IsCompactOperator.isCompact_closure_image_ball

added theorem IsCompactOperator.isCompact_closure_image_closedBall

added theorem IsCompactOperator.isCompact_closure_image_of_bounded

added theorem IsCompactOperator.isCompact_closure_image_of_vonN_bounded

added theorem IsCompactOperator.neg

added theorem IsCompactOperator.restrict'

added theorem IsCompactOperator.restrict

added theorem IsCompactOperator.smul

added theorem IsCompactOperator.sub

added def IsCompactOperator

added def compactOperator

added theorem compactOperator_topologicalClosure

added theorem isClosed_setOf_isCompactOperator

added theorem isCompactOperator_iff_exists_mem_nhds_image_subset_compact

added theorem isCompactOperator_iff_exists_mem_nhds_isCompact_closure_image

added theorem isCompactOperator_iff_image_ball_subset_compact

added theorem isCompactOperator_iff_image_closedBall_subset_compact

added theorem isCompactOperator_iff_isCompact_closure_image_ball

added theorem isCompactOperator_iff_isCompact_closure_image_closedBall

added theorem isCompactOperator_of_tendsto

added theorem isCompactOperator_zero