Subsets of the real numbers

Content created by Louis Wasserman.

Created on 2025-08-30.
Last modified on 2025-09-03.

module real-numbers.subsets-real-numbers where
Imports 
open import foundation.action-on-identifications-functions
open import foundation.dependent-pair-types
open import foundation.equivalences
open import foundation.function-extensionality
open import foundation.function-types
open import foundation.identity-types
open import foundation.images-subtypes
open import foundation.inhabited-subtypes
open import foundation.inhabited-types
open import foundation.involutions
open import foundation.logical-equivalences
open import foundation.sets
open import foundation.subtypes
open import foundation.transport-along-identifications
open import foundation.universe-levels

open import logic.functoriality-existential-quantification

open import metric-spaces.equality-of-metric-spaces
open import metric-spaces.images-isometries-metric-spaces
open import metric-spaces.isometries-metric-spaces
open import metric-spaces.metric-spaces
open import metric-spaces.subspaces-metric-spaces

open import real-numbers.dedekind-real-numbers
open import real-numbers.isometry-negation-real-numbers
open import real-numbers.metric-space-of-real-numbers
open import real-numbers.negation-real-numbers

Idea

A subset of the real numbers is a subtype.

Definition

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

type-subset-ℝ : {l1 l2 : Level} → subset-ℝ l1 l2 → UU (l1 ⊔ lsuc l2)
type-subset-ℝ = type-subtype

inclusion-subset-ℝ :
  {l1 l2 : Level} → (S : subset-ℝ l1 l2) → type-subset-ℝ S → ℝ l2
inclusion-subset-ℝ = inclusion-subtype

is-inhabited-subset-ℝ : {l1 l2 : Level} → subset-ℝ l1 l2 → UU (l1 ⊔ lsuc l2)
is-inhabited-subset-ℝ = is-inhabited-subtype

Properties

Subsets of the real numbers are sets

abstract
  is-set-subset-ℝ :
    {l1 l2 : Level} → (S : subset-ℝ l1 l2) → is-set (type-subset-ℝ S)
  is-set-subset-ℝ S = is-set-type-subtype S (is-set-type-Set (ℝ-Set _))

The metric space associated with a subset of the real numbers

metric-space-subset-ℝ :
  {l1 l2 : Level} → subset-ℝ l1 l2 → Metric-Space (l1 ⊔ lsuc l2) l2
metric-space-subset-ℝ {l1} {l2} = subspace-Metric-Space (metric-space-ℝ l2)

The elementwise negation of a subset of real numbers

neg-subset-ℝ : {l1 l2 : Level} → subset-ℝ l1 l2 → subset-ℝ l1 l2
neg-subset-ℝ S = S ∘ neg-ℝ

If a subset of real numbers is inhabited, so is its elementwise negation

abstract
  neg-is-inhabited-subset-ℝ :
    {l1 l2 : Level} → (S : subset-ℝ l1 l2) → is-inhabited-subset-ℝ S →
    is-inhabited-subset-ℝ (neg-subset-ℝ S)
  neg-is-inhabited-subset-ℝ S =
    map-is-inhabited
      ( map-equiv
        ( equiv-precomp-equiv-type-subtype (equiv-is-involution neg-neg-ℝ) S))

The elementwise negation of the elementwise negation of a subset of real numbers is the original subset

abstract
  neg-neg-subset-ℝ :
    {l1 l2 : Level} → (S : subset-ℝ l1 l2) → neg-subset-ℝ (neg-subset-ℝ S) ＝ S
  neg-neg-subset-ℝ S = eq-htpy (λ x → ap S (neg-neg-ℝ x))

The elementwise negation of a subset of real numbers is isometrically equivalent to the image of the subset under elementwise negation

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

  equiv-isometric-equiv-neg-subset-im-neg-subset-ℝ :
    type-im-subtype neg-ℝ S ≃
    type-subtype (neg-subset-ℝ S)
  equiv-isometric-equiv-neg-subset-im-neg-subset-ℝ =
    equiv-has-same-elements-type-subtype
      ( im-subtype neg-ℝ S)
      ( neg-subset-ℝ S)
      ( has-same-elements-im-subtype-equiv-precomp-inv-equiv
        ( equiv-is-involution neg-neg-ℝ)
        ( S))

  is-isometry-map-equiv-isometric-equiv-neg-subset-im-neg-subset-ℝ :
    is-isometry-Metric-Space
      ( metric-space-subset-ℝ (im-subtype neg-ℝ S))
      ( metric-space-subset-ℝ (neg-subset-ℝ S))
      ( map-equiv equiv-isometric-equiv-neg-subset-im-neg-subset-ℝ)
  is-isometry-map-equiv-isometric-equiv-neg-subset-im-neg-subset-ℝ _ _ _ =
    id-iff

  isometric-equiv-neg-subset-im-neg-subset-ℝ :
    isometric-equiv-Metric-Space
      ( im-isometry-Metric-Space
        ( metric-space-subset-ℝ S)
        ( metric-space-ℝ l2)
        ( comp-isometry-Metric-Space
          ( metric-space-subset-ℝ S)
          ( metric-space-ℝ l2)
          ( metric-space-ℝ l2)
          ( isometry-neg-ℝ)
          ( isometry-inclusion-subspace-Metric-Space (metric-space-ℝ l2) S)))
      ( metric-space-subset-ℝ (neg-subset-ℝ S))
  isometric-equiv-neg-subset-im-neg-subset-ℝ =
    ( equiv-isometric-equiv-neg-subset-im-neg-subset-ℝ ,
      is-isometry-map-equiv-isometric-equiv-neg-subset-im-neg-subset-ℝ)

Recent changes