Extended Natural Numbers and Counters

This article introduces extended natural numbers, i.e. the set ℕ ∪ {+∞}, in Mizar [4], [3] and formalizes a way to list a cardinal numbers of cardinals. Both concepts have applications in graph theory.

Bibliographic Details
Main Author: Koch Sebastian
Format: Article
Language:English
Published: Sciendo 2020-10-01
Series:Formalized Mathematics
Subjects:
Online Access:https://doi.org/10.2478/forma-2020-0021
id doaj-89e92d340e8746f393254ce1bd7d6a0a
record_format Article
spelling doaj-89e92d340e8746f393254ce1bd7d6a0a2021-09-05T21:01:04ZengSciendoFormalized Mathematics1426-26301898-99342020-10-0128323924910.2478/forma-2020-0021Extended Natural Numbers and CountersKoch Sebastian0Johannes Gutenberg University, Mainz, GermanyThis article introduces extended natural numbers, i.e. the set ℕ ∪ {+∞}, in Mizar [4], [3] and formalizes a way to list a cardinal numbers of cardinals. Both concepts have applications in graph theory.https://doi.org/10.2478/forma-2020-0021cardinalsequenceextended natural numbers03e10 68v20
collection DOAJ
language English
format Article
sources DOAJ
author Koch Sebastian
spellingShingle Koch Sebastian
Extended Natural Numbers and Counters
Formalized Mathematics
cardinal
sequence
extended natural numbers
03e10 68v20
author_facet Koch Sebastian
author_sort Koch Sebastian
title Extended Natural Numbers and Counters
title_short Extended Natural Numbers and Counters
title_full Extended Natural Numbers and Counters
title_fullStr Extended Natural Numbers and Counters
title_full_unstemmed Extended Natural Numbers and Counters
title_sort extended natural numbers and counters
publisher Sciendo
series Formalized Mathematics
issn 1426-2630
1898-9934
publishDate 2020-10-01
description This article introduces extended natural numbers, i.e. the set ℕ ∪ {+∞}, in Mizar [4], [3] and formalizes a way to list a cardinal numbers of cardinals. Both concepts have applications in graph theory.
topic cardinal
sequence
extended natural numbers
03e10 68v20
url https://doi.org/10.2478/forma-2020-0021
work_keys_str_mv AT kochsebastian extendednaturalnumbersandcounters
_version_ 1717781727244451840