Mathlib Map

Theorems · Inductive type · general topology

Filter.Realizer

{α : Type u_1} → Filter α → Type (max u_1 (u_5 + 1))

A realizer for filter f is a cfilter which generates f.

Defined in
Mathlib.Data.Analysis.Filter
Cited by
13 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.

Filter.Realizer.σ · cited by 18Realizer.σFilter.Realizer.F · cited by 12Realizer.FFilter.Realizer.bot · cited by 3Realizer.botFilter.Realizer.map · cited by 3Realizer.mapCtop.Realizer.nhds · cited by 3Realizer.nhdsFilter.Realizer.le_iff · cited by 2Realizer.le_iffFilter.Realizer.ofEquiv · cited by 2Realizer.ofEquivFilter.Realizer.principal · cited by 2Realizer.principalFilter.Realizer.top · cited by 2Realizer.topFilter.Realizer.mk.inj · cited by 1mk.injFilter.Realizer.casesOn · cited by 1Realizer.casesOnFilter.Realizer.mk.noConfusion · cited by 1mk.noConfusionFilter.Realizer.mem_sets · cited by 1Realizer.mem_setsFilter.Realizer.tendsto_iff · cited by 1Realizer.tendsto_iffFilter.Realizer.bind · cited by 0Realizer.bindFilter · cited by 8121FilterFilter.RealizerCITED BYCITES

Cites1

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

  • Filterstatement · cited by 8,121

Cited by38

Results whose statement or proof uses this declaration.