Theorems · Definition · Lie groups
AddGroupFilterBasis.toFilterBasis
{A : Type u} → {inst : AddGroup A} → [self : AddGroupFilterBasis A] → FilterBasis A- Defined in
- Mathlib.Topology.Algebra.FilterBasis
- Cited by
- 32 results in Mathlib
- Foundations
- Depth 2 from the axioms · uses no axioms
- Assumes
- AddGroupFilterBasis
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites3
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- AddGroupstatement and proof · cited by 4,410
- AddGroupFilterBasisstatement and proof · cited by 27
- FilterBasisstatement · cited by 23
Cited by43
Results whose statement or proof uses this declaration.
- SeminormFamily.withSeminorms_iff_nhds_eq_iInfproof · cited by 8
- AddGroupFilterBasis.nhds_zero_hasBasisproof · cited by 6
- AddGroupFilterBasis.nhds_zero_eqstatement and proof · cited by 4
- SeminormFamily.withSeminorms_of_nhdsstatement and proof · cited by 3
- AddGroupFilterBasis.Nproof · cited by 3
- AddGroupFilterBasis.nhds_eqproof · cited by 3
- IsAdic.isHausdorff_iffproof · cited by 2
- withSeminorms_iff_mem_nhds_isVonNBoundedproof · cited by 1
- RingFilterBasis.mul'statement · cited by 1
- RingFilterBasis.mul_left'statement · cited by 1
- RingFilterBasis.mul_right'statement · cited by 1
- ModuleFilterBasis.mk.injstatement and proof · cited by 1