Theorems · Inductive type · general topology
CFilter
(α : Type u_1) → Type u_2 → [PartialOrder α] → Type (max u_1 u_2)
A CFilter α σ is a realization of a filter (base) on α,
represented by a type σ together with operations for the top element and
the binary inf operation.
- Defined in
- Mathlib.Data.Analysis.Filter
- Cited by
- 12 results in Mathlib
- Foundations
- Depth 1 from the axioms · uses no axioms
- Assumes
- PartialOrder
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites1
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- PartialOrderstatement · cited by 6,410
Cited by30
Results whose statement or proof uses this declaration.
- CFilter.fstatement and proof · cited by 16
- Filter.Realizer.Fstatement · cited by 12
- CFilter.toFilterstatement and proof · cited by 6
- CFilter.infstatement and proof · cited by 2
- Filter.Realizer.mk.injstatement and proof · cited by 1
- Filter.Realizer.mk.noConfusionstatement and proof · cited by 1
- Filter.Realizer.casesOnstatement and proof · cited by 1
- Filter.Realizer.mem_setsproof · cited by 1
- CFilter.casesOnstatement and proof · cited by 1
- CFilter.mk.injstatement · cited by 1
- CFilter.ofEquivstatement and proof · cited by 1
- CFilter.mk.noConfusionstatement · cited by 1