Finitely enumerable subsets of the real numbers

Content created by Louis Wasserman.

Created on 2025-09-03.
Last modified on 2025-09-06.

module real-numbers.finitely-enumerable-subsets-real-numbers where
Imports 
open import foundation.dependent-pair-types
open import foundation.involutions
open import foundation.subtypes
open import foundation.universe-levels

open import real-numbers.dedekind-real-numbers
open import real-numbers.negation-real-numbers
open import real-numbers.subsets-real-numbers

open import univalent-combinatorics.finitely-enumerable-subtypes
open import univalent-combinatorics.finitely-enumerable-types

Idea

A subset of the real numbers is finitely enumerable if it is finitely enumerable as a subtype of the real numbers.

Definition

finitely-enumerable-subset-ℝ : (l1 l2 : Level) → UU (lsuc l1 ⊔ lsuc l2)
finitely-enumerable-subset-ℝ l1 l2 = finitely-enumerable-subtype l1 (ℝ l2)

module _
  {l1 l2 : Level} (S : finitely-enumerable-subset-ℝ l1 l2)
  where

  subset-finitely-enumerable-subset-ℝ : subset-ℝ l1 l2
  subset-finitely-enumerable-subset-ℝ = subtype-finitely-enumerable-subtype S

  type-finitely-enumerable-subset-ℝ : UU (l1 ⊔ lsuc l2)
  type-finitely-enumerable-subset-ℝ =
    type-subtype subset-finitely-enumerable-subset-ℝ

  is-finitely-enumerable-finitely-enumerable-subset-ℝ :
    is-finitely-enumerable-subtype subset-finitely-enumerable-subset-ℝ
  is-finitely-enumerable-finitely-enumerable-subset-ℝ =
    is-finitely-enumerable-subtype-finitely-enumerable-subtype S

  inclusion-finitely-enumerable-subset-ℝ :
    type-finitely-enumerable-subset-ℝ → ℝ l2
  inclusion-finitely-enumerable-subset-ℝ =
    inclusion-subtype subset-finitely-enumerable-subset-ℝ

Properties

The elementwise negation of a finitely enumerable subset of real numbers

neg-finitely-enumerable-subset-ℝ :
  {l1 l2 : Level} →
  finitely-enumerable-subset-ℝ l1 l2 → finitely-enumerable-subset-ℝ l1 l2
neg-finitely-enumerable-subset-ℝ (S , is-finitely-enumerable-S) =
  ( neg-subset-ℝ S ,
    is-finitely-enumerable-equiv
      ( equiv-precomp-equiv-type-subtype (equiv-is-involution neg-neg-ℝ) S)
      ( is-finitely-enumerable-S))

Recent changes