Elementary numerosity and measures

VIERI BENCI, EMANUELE BOTTAZZI, and MAURO DI NASSO

We construct a cardinality map from the powerset of any Fintype to the hyperreals.

def size {B : Type} [Fintype B] : Finset B → ℝ*

Cardinality of a finite set, as a hyperreal.

Equations

• size S = ↑↑S.card

theorem size_empty {B : Type} [Fintype B] : size ∅ = 0

The cardinality of the empty set, as a hyperreal.

theorem size_univ : size Finset.univ = 2

The cardinality of Bool, as a hyperreal.

theorem size_single {B : Type} [Fintype B] (b : B) : size {b} = 1

The cardinality of a singleton, as a hyperreal.