Grace/Cumulus/Real/Defs.g17
Imports
Declarations
- ProperSubset predicate
- DedekindCut predicate
- ℝ def
- Real class
- RealLess predicate
- realLess def
- rationalCut def
Source
1-- Dedekind real numbers2-- Part of Cumulus, the Grace17 mathematics library.3-- Copyright (c) 2026 Grant Passmore.4-- Released under the Apache License 2.0. See LICENSE in the repository root.5-- Authors: Grant Passmore67module Grace.Cumulus.Real.Defs8import Rat.OrderedOperations910predicate ProperSubset (A B : Set) := (A ⊆ B) ∧ A ≠ B11notation infix 50 "⊂" => ProperSubset1213-- A real is a lower Dedekind cut of the rational quotient set. The order used14-- here is the set-valued graph rationalLess.15predicate DedekindCut (A : Set) :=16 (A ⊆ ℚ) ∧ Nonempty(A) ∧ A ≠ ℚ ∧17 (∀ q ∈ A, ∀ p ∈ ℚ, p < q → p ∈ A) ∧18 (∀ q ∈ A, ∃ r ∈ A, relates(rationalLess, q, r))1920def ℝ : Set := { A ∈ 𝒫(ℚ) | DedekindCut(A) }21class Real (x : Set) := x ∈ ℝ2223-- Strict real order is proper inclusion of lower cuts. The predicate-level24-- view remains useful alongside the instance-selected `<` relation graph.25predicate RealLess (x y : Set) := Real(x) ∧ Real(y) ∧ (x ⊂ y)2627-- The set-valued graph used by algebraic structures and relation theory.28-- RealLess remains the convenient proposition-level view.29def realLess : Set :=30 { p ∈ ℝ × ℝ |31 ∃ x ∈ ℝ, ∃ y ∈ ℝ, p = (x, y) ∧ (x ⊂ y) }3233-- The rational q determines its lower initial segment. Once rationalLess is34-- proved dense and unbounded, rationalCut(q) is the canonical Q → R map.35def rationalCut (q : Set) : Set :=36 { p ∈ ℚ | relates(rationalLess, p, q) }37