[Merged by Bors] - feat: infinite normed field is noncompact #8349
Conversation
urkud
added
awaiting-review
| exact ⟨fun h ↦ NormedSpace.unbounded_univ 𝕜 E h.isBounded⟩ | ||
| · push_neg at H | ||
| rcases exists_ne (0 : E) with ⟨x, hx⟩ | ||
| suffices ClosedEmbedding (Infinite.natEmbedding 𝕜 · • x) from this.noncompactSpace |
There was a problem hiding this comment.
That would be good to have these closed embeddings in general? and even in finite dimension.
There was a problem hiding this comment.
What general statement are you talking about? https://leanprover-community.github.io/mathlib4_docs/Mathlib/Topology/Algebra/Module/FiniteDimension.html#closedEmbedding_smul_left ? Another statement is that a trivially normed field has discrete topology (so, in fact we can skip Infinite.natEmbedding 𝕜).
There was a problem hiding this comment.
I was thinking of the suffices that you prove on the next lines. I guess it also holds when the field is nontrivially valued.
Actually, I am not sure you need to make the cases disjoint: once you reduce to the case of a line by these closed embeddings, what matters is that k is noncompact.
There was a problem hiding this comment.
If k = Q, then this scalar multiplication is not a closed embedding.
|
bors r+ |
github-actions
bot
added
ready-to-merge
Generalize from nontrivially normed fields to normed fields. Also prove that a nontrivially normed field is infinite.
|
Pull request successfully merged into master. Build succeeded: |
mathlib-bors
bot
changed the title
Generalize from nontrivially normed fields to normed fields. Also prove that a nontrivially normed field is infinite.
Generalize from nontrivially normed fields to normed fields. Also prove that a nontrivially normed field is infinite.
Generalize from nontrivially normed fields to normed fields. Also prove that a nontrivially normed field is infinite.
Generalize from nontrivially normed fields to normed fields.
Also prove that a nontrivially normed field is infinite.