Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-07-28 21:09 4ff8c3db

View on Github →

feat(analysis/normed_space/compact_operator): definition and basic facts about compact operators (#15467)

Estimated changes

Created src/analysis/normed_space/compact_operator.lean

added def compact_operator

added theorem compact_operator_topological_closure

added theorem continuous_linear_map.coe_mk_of_is_compact_operator

added def continuous_linear_map.mk_of_is_compact_operator

added theorem continuous_linear_map.mk_of_is_compact_operator_mem_compact_operator

added theorem continuous_linear_map.mk_of_is_compact_operator_to_linear_map

added theorem is_closed_set_of_is_compact_operator

added theorem is_compact_operator.add

added theorem is_compact_operator.clm_comp

added theorem is_compact_operator.cod_restrict

added theorem is_compact_operator.comp_clm

added theorem is_compact_operator.continuous

added theorem is_compact_operator.continuous_comp

added theorem is_compact_operator.image_ball_subset_compact

added theorem is_compact_operator.image_closed_ball_subset_compact

added theorem is_compact_operator.image_subset_compact_of_bounded

added theorem is_compact_operator.image_subset_compact_of_vonN_bounded

added theorem is_compact_operator.is_compact_closure_image_ball

added theorem is_compact_operator.is_compact_closure_image_closed_ball

added theorem is_compact_operator.is_compact_closure_image_of_bounded

added theorem is_compact_operator.is_compact_closure_image_of_vonN_bounded

added theorem is_compact_operator.neg

added theorem is_compact_operator.restrict'

added theorem is_compact_operator.restrict

added theorem is_compact_operator.smul

added theorem is_compact_operator.sub

added def is_compact_operator

added theorem is_compact_operator_iff_exists_mem_nhds_image_subset_compact

added theorem is_compact_operator_iff_exists_mem_nhds_is_compact_closure_image

added theorem is_compact_operator_iff_image_ball_subset_compact

added theorem is_compact_operator_iff_image_closed_ball_subset_compact

added theorem is_compact_operator_iff_is_compact_closure_image_ball

added theorem is_compact_operator_iff_is_compact_closure_image_closed_ball

added theorem is_compact_operator_of_tendsto

added theorem is_compact_operator_zero