Uncountable sets

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

Created on 2022-05-13.
Last modified on 2024-09-23.

module set-theory.uncountable-sets where
Imports 
open import foundation.negation
open import foundation.propositions
open import foundation.sets
open import foundation.universe-levels

open import set-theory.countable-sets

Idea

A set X is uncountable if X is not empty and there is no surjection ℕ ↠ X. In other words, if X is not countable.

Definition

is-uncountable-Prop : {l : Level} → Set l → Prop l
is-uncountable-Prop X = neg-Prop (is-countable-Prop X)

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

is-prop-is-uncountable : {l : Level} (X : Set l) → is-prop (is-uncountable X)
is-prop-is-uncountable X = is-prop-type-Prop (is-uncountable-Prop X)

Recent changes