Structures · Topology
AddGroupFilterBasis
An AddGroupFilterBasis on an additive group is a FilterBasis satisfying some additional
axioms. Example : if G is a topological group then the neighbourhoods of the identity are an
AddGroupFilterBasis. Conversely given an AddGroupFilterBasis one can define a topology
compatible with the group structure on G.
- Defined in
- Mathlib.Topology.Algebra.FilterBasis
- Shape
- One type argument · adds zero', add', neg', conj'
Extends0
Extends nothing: this is a root of the hierarchy.
Extended by1
Concrete types that are instances0
No instance on a concrete type; it is reached through other classes.
How is a type an instance?
Loading the hierarchy index…
Assumed by6
Ancestors0
No ancestors.