Infinite sets

Content created by Jonathan Prieto-Cubides, Fredrik Bakke and Egbert Rijke.

Created on 2022-09-15.
Last modified on 2024-09-23.

module set-theory.infinite-sets where
Imports 
open import elementary-number-theory.natural-numbers

open import foundation.dependent-pair-types
open import foundation.mere-embeddings
open import foundation.propositions
open import foundation.sets
open import foundation.universe-levels

open import univalent-combinatorics.standard-finite-types

Idea

A set A is said to be infinite if it contains arbitrarily large finite subsets.

Definition

The predicate on a set of being infinite

is-infinite-Set-Prop : {l : Level} → Set l → Prop l
is-infinite-Set-Prop X = Π-Prop ℕ (λ n → mere-emb-Prop (Fin n) (type-Set X))

is-infinite-Set : {l : Level} → Set l → UU l
is-infinite-Set X = type-Prop (is-infinite-Set-Prop X)

The universe of infinite sets

Infinite-Set : (l : Level) → UU (lsuc l)
Infinite-Set l = Σ (Set l) (is-infinite-Set)

module _
  {l : Level} (X : Infinite-Set l)
  where

  set-Infinite-Set : Set l
  set-Infinite-Set = pr1 X

  type-Infinite-Set : UU l
  type-Infinite-Set = type-Set set-Infinite-Set

  is-infinite-Infinite-Set : is-infinite-Set set-Infinite-Set
  is-infinite-Infinite-Set = pr2 X

Recent changes