Topological vector spaces over the reals are contractible

[GeoffreySangston]

This could be an alternative proof for S176|P199 and S30|P199, from #886 (comment)

Edit: I should assert that it is a real topological vector space.

Edit: Added S21|P199 (weak topology on separable Hilbert space).

[prabau]

I agree with this change. But note that S106 is in the process of being merged with S30. See #863.
So maybe this can wait until after that, and then applied to S30 instead.

[yhx-12243]

In fact the pull request of adding P199 to S30 is already in #886, so this pull request will automatically closed once #863 is resolved successfully.

[GeoffreySangston]

I agree with this change. But note that S106 is in the process of being merged with S30. See #863. So maybe this can wait until after that, and then applied to S30 instead.

In fact the pull request of adding P199 to S30 is already in #886, so this pull request will automatically closed once #863 is resolved successfully.

Ah I missed these somehow. Maybe we should just close this PR then and add S21|P199 after.

[prabau]

You can mark this one as draft for now and then revisit after #863 is merged.

[prabau]

Do you want to do an associated cleanup for traits that are derivable from Contractible here, or leave that for later?

[GeoffreySangston]

Do you want to do an associated cleanup for traits that are derivable from Contractible here, or leave that for later?

I could do either, but later may be later than is desirable.

[prabau]

Yeah, when adding new traits, we usually do associated cleanup at the same time, so it shows a tidier minimal set of traits. Sometimes, but totally optional, even a little more (e.g., the space being not Indiscrete).

[GeoffreySangston]

I've converted to a draft until I find time to do the cleanup.

[GeoffreySangston]

Is there any reason to keep S30|P53 (metrizable) and S30|P55 (completely metrizable)?

[prabau]

Is there any reason to keep S30|P53 (metrizable) and S30|P55 (completely metrizable)?

No reason. Feel free to clean up anything obvious or more.

[GeoffreySangston]

The following is a mistake, because the space actually satisfies ~pseudocompact. So let me figure out how to revert the last commits and then redo the search for minimal assumptions with that assumption instead. I know that in the terminal I could call 'git revert ', just figuring out how to do it with the gitdev browser IDE. It looks like the only option is to paste the files back and make another commit.

(Had another comment but there was another typo so I don't think it's worth anybody's time to read it, and I deleted it.)

---

Looks like completely metrizable + pseudocompact makes $\sigma$-compact redundant.

π-Base, Search for completely metrizable + ~$\sigma$-compact + Pseudocompact

Also completely metrizable + pseudocompact implies weakly locally compact

π-Base, Search for completely metrizable + ~weakly locally compact + Pseudocompact

Same for separable

π-Base, Search for completely metrizable + ~separable + Pseudocompact

That appears to be all of the redundant traits.

[GeoffreySangston]

Resetting...

The following says that pseudocompact = false is redundant. Going to hold off on deleting it so I can double check later.
π-Base, Search for pseudocompact + ~weakly locally compact + completely metrizable + ~Indiscrete

(Actually 'Indiscrete' was irrelevant in this search.)

So 'pseudocompact' could be deleted. The direct argument of 'Hilbert space is not pseudocompact' is obvious from the definitions, so there's no interesting direct argument being lost if I delete it. Then again, deducing it from the other properties leads to a tedious sequence of reductions. Should I delete it?

[prabau]

Approving as is.

Even this simpler search π-Base, Search for metrizable + ~WLC + pseudocompact
to derive [Metrizable + not weakly locally compact ==> not pseudocompact] is really a bear.

We can leave it for now, but I wish there was an easier derivation. @StevenClontz Any comment?

I also wonder how to revert a commit from github.dev.