Who came up with group filter bases?

Stream: maths

[Sebastian Monnet]

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]

It is very explicitly in Bourbaki

[Patrick Massot]

General topology, chapter 3, Section 1.2

[Patrick Massot]

Proposition 1