Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-01-08 18:36 09f69890

View on Github →

chore(analysis/normed_space/banach): move more to the continuous_linear_map NS (#11263)

Rename

  • open_mappingcontinuous_linear_map.is_open_map;
  • open_mapping_affineaffine_map.is_open_map;

New lemmas

  • continuous_linear_map.quotient_map,
  • continuous_linear_map.interior_preimage,
  • continuous_linear_map.closure_preimage,
  • continuous_linear_map.frontier_preimage.

Estimated changes