Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-03-09 10:19 4258f5ee

View on Github →

refactor(analysis/normed_space/banach): use bundled →L[𝕜] maps (#2107)

Estimated changes

Modified src/analysis/normed_space/banach.lean

modified theorem exists_approx_preimage_norm_le

modified theorem exists_preimage_norm_le

added theorem linear_equiv.continuous_symm

deleted theorem linear_equiv.is_bounded_inv

modified theorem open_mapping