Mathlib Map

Theorems · Definition · general topology

CFilter.toFilter

{α : Type u_1} → {σ : Type u_3} → CFilter (Set α) σ → Filter α

The filter represented by a CFilter is the collection of supersets of elements of the filter base.

Defined in
Mathlib.Data.Analysis.Filter
Cited by
6 results in Mathlib
Foundations
Depth 62 from the axioms · uses propext, Classical.choice, Quot.sound
Mathlib docsSourceLoogleLeanSearch

Around this declaration

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

Filter.Realizer.mem_sets · cited by 1Realizer.mem_setsFilter.Realizer.mk.inj · cited by 1mk.injFilter.Realizer.mk.noConfusion · cited by 1mk.noConfusionFilter.Realizer.casesOn · cited by 1Realizer.casesOnFilter.Realizer.noConfusion · cited by 0Realizer.noConfusionFilter.Realizer.noConfusionType · cited by 0Realizer.noConfusionTypeCFilter.mem_toFilter_sets · cited by 0CFilter.mem_toFilter_setsFilter.Realizer.recOn · cited by 0Realizer.recOnFilter.Realizer.mk.injEq · cited by 0mk.injEqFilter.Realizer.mk.sizeOf_spec · cited by 0mk.sizeOf_specCFilter.toRealizer · cited by 0CFilter.toRealizerFilter.Realizer.eq · cited by 0Realizer.eqSet · cited by 53352SetFilter · cited by 8121FilterSet.ofPred · cited by 6101Set.ofPredCFilter.f · cited by 16CFilter.fCFilter · cited by 12CFilterCFilter.toFilterCITED BYCITES

Cites5

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

  • Setstatement and proof · cited by 53,352
  • Filterstatement · cited by 8,121
  • Set.ofPredproof · cited by 6,101
  • CFilter.fproof · cited by 16
  • CFilterstatement and proof · cited by 12

Cited by12

Results whose statement or proof uses this declaration.