theorem SetTheory.Cardinality.n_lt_two_pow_n (n : ℕ) : n < 2 ^ n

Corollary to Cantor's theorem: for every natural number n, n < 2 ^ n.

def SetTheory.Cardinality.SameCardinality (A : Type u_1) (B : Type u_2) : Prop

SameCardinality A B states that A and B have the same cardinality, i.e. there exists a bijection between them (A ≃ B).

theorem SetTheory.Cardinality.cantor_cardinal (α : Type u_1) : Cardinal.mk α < Cardinal.mk (Set α)

Cantor's theorem: for every type α, the cardinality of α is strictly less than the cardinality of its power set Set α.

theorem SetTheory.Cardinality.cantor_schroeder_bernstein {α : Type u_1} {β : Type u_2} (f : α → β) (g : β → α) (hf : Function.Injective f) (hg : Function.Injective g) : Nonempty (α ≃ β)

Cantor-Schröder-Bernstein theorem: if there are injections f : α → β and g : β → α, then there exists a bijection between α and β; equivalently, |α| ≤ |β| and |β| ≤ |α| imply |α| = |β|.