Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-04-11 01:51 c6e62cfe

View on Github →

feat(analysis/normed_space/finite_dimension): set of f : E →L[𝕜] F of rank ≥n is open (#7022)

Estimated changes

Modified src/analysis/normed_space/basic.lean

added theorem antilipschitz_with.add_sub_lipschitz_with

Modified src/analysis/normed_space/finite_dimension.lean

added theorem is_open_set_of_linear_independent

added theorem is_open_set_of_nat_le_rank

added theorem linear_map.exists_antilipschitz_with

Modified src/analysis/normed_space/operator_norm.lean

added theorem continuous_linear_equiv.nnnorm_symm_pos

Modified src/data/finsupp/basic.lean

modified def finsupp.equiv_fun_on_fintype

Modified src/linear_algebra/basic.lean

added theorem linear_map.coe_smul_right

modified theorem linear_map.smul_right_apply

Modified src/linear_algebra/finite_dimensional.lean

Modified src/linear_algebra/linear_independent.lean

added theorem fintype.linear_independent_iff'

Modified src/linear_algebra/pi.lean

modified def linear_map.lsum