Zulip Chat Archive
Stream: mathlib4
Topic: loop space notation
Kevin Buzzard (Jul 04 2023 at 16:00):
The measure theorists / probabilists aren't going to like
scoped[Topology] notation "Ω" => LoopSpace
in Topology.Homotopy.HomotopyGroup...
(indeed a probabilist is currently complaining about this on the Discord...)
I guess they just avoid importing HomotopyGroup. They did this because a coercion was missing for them so I told them to import Mathlib to ensure they had it.
Matthew Ballard (Jul 04 2023 at 16:05):
This is pretty standard notation. Though I could see it scoped to Topology.Homotopy
Kevin Buzzard (Jul 04 2023 at 16:10):
The probabilist would observe that Omega is also pretty standard notation in probability theory, and topology needs to be opened so you can have neighbourhood filter notation
Kyle Miller (Jul 04 2023 at 16:15):
Having it be scoped to Topology.Homotopy seems like a good idea to me
Matthew Ballard (Jul 04 2023 at 17:36):
Notification Bot (Jul 04 2023 at 17:36):
A message was moved here from #mathlib4 > Proposed refactor of Bitvec by Matthew Ballard.
Last updated: Dec 20 2023 at 11:08 UTC