Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2019-04-30 12:53 8dcce05f

View on Github →

feat(analysis/normed_space): open mapping (#900)

The Banach open mapping theorem
improve comments
feat(analysis/normed_space): rebase, fix build

Estimated changes

Created src/analysis/normed_space/banach.lean

added theorem exists_preimage_norm_le

added theorem linear_equiv.is_bounded_inv

added theorem open_mapping

Modified src/analysis/specific_limits.lean

added theorem has_sum_geometric_two'

modified theorem has_sum_geometric_two

added theorem summable_geometric

added theorem summable_geometric_two

added theorem tsum_geometric

added theorem tsum_geometric_two