eventually_cocardinal_notMem — Mathlib

English

For any finite set s, almost all elements of cocardinal avoid s.

Русский

Для любого конечного множества s почти все элементы cocardinal не принадлежат s.

LaTeX

$$Finset.eventually_cocardinal_notMem (s : Finset α) : ∀ᶠ x in cocardinal α hreg, x ∉ s$$

Lean4

theorem _root_.Finset.eventually_cocardinal_notMem (s : Finset α) : ∀ᶠ x in cocardinal α hreg, x ∉ s :=
  eventually_cocardinal_notMem_of_card_lt <| (finset_card_lt_aleph0 s).trans_le (hreg.aleph0_le)

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