English
The comk construction defines a filter from a predicate p by taking as sets those whose complements satisfy p; this is a standard cofinite-like construction.
Русский
Конструктор comk строит фильтр из предиката p, беря в качестве множеств те множества, чьи комплементы удовлетворяют p.
LaTeX
$$$\text{def }\text{comk}(p,\,he,\,hmono,\,hunion):\text{Filter } α$ where\ sets := \{t\mid p(t^c)\}$$$
Lean4
/-- 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`. -/
def comk (p : Set α → Prop) (he : p ∅) (hmono : ∀ t, p t → ∀ s ⊆ t, p s) (hunion : ∀ s, p s → ∀ t, p t → p (s ∪ t)) :
Filter α where
sets := {t | p tᶜ}
univ_sets := by simpa
sets_of_superset := fun ht₁ ht => hmono _ ht₁ _ (compl_subset_compl.2 ht)
inter_sets := fun ht₁ ht₂ => by simp [compl_inter, hunion _ ht₁ _ ht₂]
