mk_compl_of_infinite — Mathlib

English

If α is infinite and a subset s has strictly smaller cardinality than α, then the complement s^c also has cardinality α.

Русский

Если α бесконечно и подмножество s имеет строго меньшую кардинальность, то комплемент s^c также имеет кардинальность α.

LaTeX

$$$|s^{c}| = |\\alpha|$$$

Lean4

theorem mk_compl_of_infinite {α : Type*} [Infinite α] (s : Set α) (h2 : #s < #α) : #(sᶜ : Set α) = #α :=
  by
  refine eq_of_add_eq_of_aleph0_le ?_ h2 (aleph0_le_mk α)
  exact mk_sum_compl s

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