Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-01-07 13:09 3aea2845

View on Github →

feat(analysis/normed_space): affine map with findim domain is continuous (#5627)

Estimated changes

Modified src/analysis/normed_space/add_torsor.lean

added theorem affine_map.continuous_linear_iff

Modified src/analysis/normed_space/basic.lean

added theorem dist_eq_norm'

Modified src/analysis/normed_space/finite_dimension.lean

added theorem affine_map.continuous_of_finite_dimensional

Modified src/analysis/normed_space/operator_norm.lean

added theorem continuous_linear_map.apply_apply