Infinite sets
Content created by Jonathan Prieto-Cubides, Fredrik Bakke and Egbert Rijke.
Created on 2022-09-15.
Last modified on 2023-03-14.
module set-theory.infinite-sets where
Imports
open import elementary-number-theory.natural-numbers 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
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)
Recent changes
- 2023-03-14. Fredrik Bakke. Remove all unused imports (#502).
- 2023-03-13. Jonathan Prieto-Cubides. More maintenance (#506).
- 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).