Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2019-11-03 15:40 a6ace342

View on Github →

feat(analysis/normed_space): Riesz's lemma (#1642)

  • fix(topology/metric_space/hausdorff_distance): fix typo
  • feat(analysis/normed_space): Riesz's Lemma
  • fix(analysis/normed_space): fix silly mistake in statement of riesz lemma
  • style(analysis/normed_space/riesz_lemma): variable names & indent
  • doc(analysis/normed_space/riesz_lemma): add attribution
  • doc(analysis/normed_space/riesz_lemma): fix module docstring style
  • style(analysis/normed_space/riesz_lemma): more style & documentation
  • recall statement in module header comment
  • typecast instead of unfold

Estimated changes