English
There is a realizer for the cofinite filter on α. Its index set is finite subsets of α, and the value at a finite set s is the set of elements not in s.
Русский
Существует реализатор для кофинитного фильтра на α: индексное множество состоит из конечных подмножеств α, а значение в таком множестве s состоит из элементов, не принадлежащих s.
LaTeX
$$$\\text{Realizer}({\\text{cofinite}})(α) = \\langle \\text{Finset } α, \\; f(s) = \\{ a : α \\mid a \\notin s \\}, \\; \\text{pt} = ∅, \\; \\text{inf} = (\\cdot \\cup \\cdot) \\rangle$$$
Lean4
/-- Construct a realizer for the cofinite filter -/
protected def cofinite [DecidableEq α] : (@cofinite α).Realizer :=
⟨Finset α,
{ f := fun s ↦ {a | a ∉ s}
pt := ∅
inf := (· ∪ ·)
inf_le_left := fun _ _ _ ↦ mt (Finset.mem_union_left _)
inf_le_right := fun _ _ _ ↦ mt (Finset.mem_union_right _) },
filter_eq <|
Set.ext fun _ ↦ ⟨fun ⟨s, h⟩ ↦ s.finite_toSet.subset (compl_subset_comm.1 h), fun h ↦ ⟨h.toFinset, by simp⟩⟩⟩
