Zulip Chat Archive

Stream: maths

Topic: Who came up with group filter bases?


Sebastian Monnet (May 11 2022 at 16:08):

The structure group_filter_basis in Lean was written by @Patrick Massot. The general reference for topology/algebra/filter_basis is "General Topology" by Bourbaki, but I haven't been able to find mention of group filter bases in there - I've also looked for the same structure under a different name, but obviously it's difficult to do that without reading the whole book. Was Massot the first person to write down explicitly the axioms of a group filter basis, or are they somewhere in Bourbaki/elsewhere?

Patrick Massot (May 11 2022 at 17:08):

It is very explicitly in Bourbaki

Patrick Massot (May 11 2022 at 17:11):

General topology, chapter 3, Section 1.2

Patrick Massot (May 11 2022 at 17:12):

Proposition 1


Last updated: Dec 20 2023 at 11:08 UTC