Mathlib Map

Theorems · Definition · general topology

FilterBasis.sets

{α : Type u_6} → FilterBasis α → Set (Set α)

Sets of a filter basis.

Defined in
Mathlib.Order.Filter.Bases.Basic
Cited by
42 results in Mathlib
Foundations
Depth 1 from the axioms · uses no axioms
Mathlib docsSourceLoogleLeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

FilterBasis.generate · cited by 4FilterBasis.generateUniformFun.gc · cited by 2UniformFun.gcFilter.FilterBasis.ofSets_sets · cited by 2FilterBasis.ofSets_setsFilterBasis.inter_sets · cited by 2FilterBasis.inter_setsFilterBasis.ker_filter · cited by 2FilterBasis.ker_filterIsAdic.isHausdorff_iff · cited by 2IsAdic.isHausdorff_iffRingFilterBasis.mul' · cited by 1RingFilterBasis.mul'RingFilterBasis.mul_left' · cited by 1RingFilterBasis.mul_left'RingFilterBasis.mul_right' · cited by 1RingFilterBasis.mul_right'RingFilterBasis.mk.congr_simp · cited by 1mk.congr_simpModuleFilterBasis.smul' · cited by 1ModuleFilterBasis.smul'ModuleFilterBasis.smul_left' · cited by 1ModuleFilterBasis.smul_le…ModuleFilterBasis.smul_right' · cited by 1ModuleFilterBasis.smul_ri…AddGroupFilterBasis.zero' · cited by 1AddGroupFilterBasis.zero'Filter.CountableFilterBasis.mk.inj · cited by 1mk.injSet · cited by 53352SetFilterBasis · cited by 23FilterBasisFilterBasis.setsCITED BYCITES

Cites2

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

  • Setstatement · cited by 53,352
  • FilterBasisstatement and proof · cited by 23

Cited by67

Results whose statement or proof uses this declaration.