Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2019-06-07 16:54 b55e44de

View on Github →

refactor(analysis/normed_space/basic): change normed_space definition (#1112)

Estimated changes

Modified src/analysis/asymptotics.lean

Modified src/analysis/convex.lean

modified theorem convex_ball

modified theorem convex_closed_ball

modified theorem convex_on_dist

Modified src/analysis/normed_space/banach.lean

Modified src/analysis/normed_space/basic.lean

added structure normed_group.core

added theorem normed_group.tendsto_nhds_zero

deleted structure normed_space.core

deleted theorem normed_space.tendsto_nhds_zero

Modified src/analysis/normed_space/bounded_linear_maps.lean

modified structure is_bounded_linear_map

Modified src/analysis/normed_space/deriv.lean

Modified src/analysis/normed_space/operator_norm.lean

added theorem continuous_linear_map.op_norm_neg