eventually_cocardinal_notMem_of_card_lt

Mathlib.Order.Filter.Cocardinal

URI: https://scilib.ai/kg/mathlib#Filter.eventually_cocardinal_notMem_of_card_lt

English

If |s| < c then eventually a ∉ s.

Русский

Если |s| < c, то почти наверняка a не принадлежит s.

LaTeX

$$eventually_cocardinal_notMem_of_card_lt {s : Set α} (hs : #s < c) : ∀ᶠ a in cocardinal α hreg, a ∉ s$$

Lean4

theorem eventually_cocardinal_notMem_of_card_lt {s : Set α} (hs : #s < c) : ∀ᶠ x in cocardinal α hreg, x ∉ s :=
  compl_mem_cocardinal_of_card_lt hs

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru