Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-09-15 00:53 82dced60

View on Github →

feat(analysis/normed_space/finite_dimension): Riesz theorem on compact unit ball and finite dimension (#9147)

Estimated changes

Modified docs/undergrad.yaml

Modified src/analysis/normed_space/basic.lean

Modified src/analysis/normed_space/finite_dimension.lean

added theorem exists_norm_le_le_norm_sub_of_finset

added theorem exists_seq_norm_le_one_le_norm_sub'

added theorem exists_seq_norm_le_one_le_norm_sub

added theorem finite_dimensional_of_is_compact_closed_ball

Modified src/analysis/normed_space/riesz_lemma.lean

added theorem riesz_lemma_of_norm_lt

Modified src/data/fintype/basic.lean

added theorem exists_seq_of_forall_finset_exists'

added theorem exists_seq_of_forall_finset_exists

Modified src/ring_theory/noetherian.lean

added theorem is_noetherian_top_iff