Theorems · Definition · general topology

Filter.comk

{α : Type u_1} →
  (p : Set α → Prop) →
    p ∅ → (∀ (t : Set α), p t → ∀ s ⊆ t, p s) → (∀ (s : Set α), p s → ∀ (t : Set α), p t → p (s ∪ t)) → Filter α

Construct a filter from a property that is stable under finite unions. A set s belongs to Filter.comk p _ _ _ iff its complement satisfies the predicate p. This constructor is useful to define filters like Filter.cofinite.

Defined in

Mathlib.Order.Filter.Defs

Cited by

6 results in Mathlib

Foundations

Depth 59 from the axioms · uses propext, Classical.choice, Quot.sound