Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2019-11-12 16:51 7b07932d

View on Github →

feat(analysis/normed_space/operator_norm): continuity of linear forms; swap directions of nnreal.coe_* (#1655)

feat(analysis/normed_space/operator_norm): continuity of linear forms
use lift, change nnreal.coe_le direction

Estimated changes

Modified src/analysis/normed_space/operator_norm.lean

added theorem continuous_linear_map.bound_of_uniform_embedding

added theorem continuous_linear_map.uniform_continuous

added theorem continuous_linear_map.uniform_embedding_of_bound

added theorem linear_equiv.uniform_embedding

added theorem linear_map.bound_of_continuous

added theorem linear_map.continuous_iff_is_closed_ker

modified theorem linear_map.continuous_of_bound

modified def linear_map.with_bound

modified theorem linear_map_with_bound_apply

modified theorem linear_map_with_bound_coe

Modified src/analysis/normed_space/riesz_lemma.lean

Modified src/data/real/ennreal.lean

Modified src/data/real/nnreal.lean

Modified src/measure_theory/decomposition.lean

Modified src/measure_theory/simple_func_dense.lean

Modified src/topology/metric_space/basic.lean

added theorem ball_pi

added theorem closed_ball_pi

added theorem dist_pi_le_iff

added theorem dist_pi_lt_iff

added theorem metric.uniform_embedding_iff'

added theorem proper_space_of_compact_closed_ball_of_le

Modified src/topology/metric_space/emetric_space.lean

added theorem emetric.uniform_embedding_iff'

Modified src/topology/metric_space/isometry.lean