mem_cofinite — Mathlib

English

Let X be a type. A subset s ⊆ X belongs to the cofinite filter on X if and only if its complement is finite.

Русский

Пусть X — множество. Подмножество s ⊆ X принадлежит кофинитному фильтру на X тогда и только тогда, когда его дополнение конечное.

LaTeX

$$$s \in \operatorname{cofinite} \Longleftrightarrow (s^{c}).Finite$$$

Lean4

@[simp]
theorem mem_cofinite {s : Set α} : s ∈ @cofinite α ↔ sᶜ.Finite :=
  Iff.rfl

Похожие утверждения