compl_mem_hyperfilter_of_finite

Mathlib.Order.Filter.Ultrafilter.Basic

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

English

If s is finite, then its complement s^c belongs to the hyperfilter.

Русский

Если s конечно, то его комплемент принадлежит hyperfilter α.

LaTeX

$$$s\text{ finite} \Rightarrow s^c \in hyperfilter(\alpha)$$$

Lean4

theorem compl_mem_hyperfilter_of_finite {s : Set α} (hf : Set.Finite s) : sᶜ ∈ hyperfilter α :=
  compl_mem_iff_notMem.2 hf.notMem_hyperfilter

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

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

Разделы

Аффилиация

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