Grace/Cumulus/Real/Rationals.g17

Open in Workbench Download source

Imports

RootTwoRational

Declarations

• rationalReals def
• sqrtTwo.not_rational theorem derivation
• Irrational predicate
• sqrtTwo.irrational theorem derivation

Source

1-- The rationals inside the reals, irrationality, and the irrationality of √22-- 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.Rationals8import RootTwoRational910-- The image of the rationals under the cut embedding; ℚ itself is the set11-- of rationals.12def rationalReals : Set := { rationalCut(q) | q ∈ ℚ }1314theorem sqrtTwo.not_rational15  shows √2 ∉ rationalReals16proof17  intro member18  obtain ⟨q, qInQ, equal⟩ := rationalReals.membership.forward with member19  symm at equal20  exact sqrtTwo.ne_rationalCut with *, equal2122-- A real number is irrational when it is not the image of any rational23-- under the embedding of ℚ into ℝ: the textbook √2 ∉ ℚ, with ℚ read as its24-- copy inside ℝ.25predicate Irrational (x : Real) := ¬(∃ q ∈ ℚ, rationalCut(q) = x)2627theorem sqrtTwo.irrational28  shows Irrational(√2)29proof30  unfold Irrational31  constructor32  . have one := realZero.lt_one33    have twoLe : (0:R) ≤ (2:R) by linarith34    have twoNonnegative := NonnegativeReal.of_le with *35    exact sqrt.real with *36  . intro rational37    obtain ⟨q, qInQ, equal⟩ := rational38    have distinct := sqrtTwo.ne_rationalCut at q with *39    symm at equal40    exact distinct with equal41