eventually_cofinite_notMem — Mathlib

English

Same as Set.Finite version, but for finite sets; every finite set eventually avoids membership in cofinite.

Русский

То же самое для конечного множества: для любого конечного множества в кофинитном фильтре почти все элементы не принадлежат этому множество.

LaTeX

$$$s \text{ finite} \Rightarrow \forall^\infty x \in \operatorname{cofinite}, x \notin s$$$

Lean4

theorem _root_.Finset.eventually_cofinite_notMem (s : Finset α) : ∀ᶠ x in cofinite, x ∉ s :=
  s.finite_toSet.eventually_cofinite_notMem

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