Irrational real numbers

Content created by Louis Wasserman.

Created on 2025-11-19.
Last modified on 2025-11-19.

{-# OPTIONS --lossy-unification #-}

module real-numbers.irrational-real-numbers where
Imports 
open import elementary-number-theory.rational-numbers

open import foundation.dependent-pair-types
open import foundation.negation
open import foundation.propositions
open import foundation.universe-levels

open import real-numbers.dedekind-real-numbers
open import real-numbers.rational-real-numbers

Idea

An irrational real number is a real number that is not rational.

Definition

is-irrational-prop-ℝ : {l : Level} → ℝ l → Prop l
is-irrational-prop-ℝ x = ¬' (subtype-rational-real x)

is-irrational-ℝ : {l : Level} → ℝ l → UU l
is-irrational-ℝ x = type-Prop (is-irrational-prop-ℝ x)

Recent changes