Uncountable sets
Content created by Jonathan Prieto-Cubides, Egbert Rijke and Fredrik Bakke.
Created on 2022-05-13.
Last modified on 2023-03-10.
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
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
- 2023-03-10. Fredrik Bakke. Additions to
fix-import
(#497). - 2023-03-09. Jonathan Prieto-Cubides. Add hooks (#495).
- 2023-03-07. Fredrik Bakke. Add blank lines between
<details>
tags and markdown syntax (#490). - 2023-03-07. Jonathan Prieto-Cubides. Show module declarations (#488).
- 2023-03-05. Jonathan Prieto-Cubides. Add "suggest an edit" button and minor fix (#484).