compl_mem_cocardinal — Mathlib

English

If s is finite then its complement belongs to cocardinal.

Русский

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

LaTeX

$$Set.Finite.compl_mem_cocardinal {s : Set α} (hs : s.Finite) : sᶜ ∈ cocardinal α hreg$$

Lean4

theorem _root_.Set.Finite.compl_mem_cocardinal {s : Set α} (hs : s.Finite) : sᶜ ∈ cocardinal α hreg :=
  compl_mem_cocardinal_of_card_lt <| lt_of_lt_of_le (Finite.lt_aleph0 hs) (hreg.aleph0_le)

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