Documentation

Marginis.BenciBottazziDiNasso2014

Elementary numerosity and measures #

by VIERI BENCI EMANUELE BOTTAZZI 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
Instances For
    theorem size_empty {B : Type} [Fintype B] :

    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.