HomeIsabelle/Phabricator

Complex_Bounded_Operators: Various changes:

Description

Complex_Bounded_Operators: Various changes:

  • Removed auxiliary constant the_riesz_rep_bilinear'
  • Renamed constant the_riesz_rep_bilinear -> the_riesz_rep_sesqui and defined differently but equivalently
  • Renamed constant bifunctional -> bidual_embedding (and renamed lemmas containing bifunctional accordingly)
  • Renamed lemmas the_riesz_rep_bilinear_apply -> the_riesz_rep_sesqui_apply, cblinfun_extension_exists_norm -> cblinfun_extension_norm_bounded_dense
  • New theorems: rank1_compose_left, rank1_compose_right, rank1_scaleC, rank1_uminus, rank1_uminus_iff, rank1_adj, rank1_adj_iff, bidual_embedding_surj, Cblinfun_comp_bounded_cbilinear, Cblinfun_comp_bounded_sesquilinear, bounded_clinear_0, bounded_antilinear_0, bounded_cbilinear_0, bounded_sesquilinear_0, bounded_cbilinear_apply_bounded_clinear, bounded_sesquilinear_apply_bounded_clinear, cblinfun_extension_exists_hilbert, trunc_ell2_reduces_norm, trunc_ell2_add, trunc_ell2_scaleC, bounded_clinear_trunc_ell2
  • Theorem cblinfun_extension_exists_proj: Reformulated one assumption

Details

Provenance
kleingAuthored on
Parents
rAFPad6ac3e1e898: slightly less abusive proof pattern
Branches
Unknown
Tags
Unknown