namespace http://mathhub.info/MitM/core/arithmetics ❚
import base http://mathhub.info/MitM/Foundation ❚
theory RealNumbers : base:?Logic =
include ☞base:?RealLiterals ❙
include ?RationalNumbers ❙
RealNumbers = ℝ ❙
axiom_ratsAreReal : ℚ <* ℝ ❙
axiom_intsAreReal : ℤ <* ℝ ❙
axiom_natsAreReal : ℕ <* ℝ ❙
axiom_posAreReal : ℕ+ <* ℝ ❙
NAT_is_real : NAT <* ℝ ❙
❚
theory RealArithmetics : base:?Logic =
include ?RealNumbers ❙
include ?RationalArithmetics ❙
/T Negation ❙
uminus : ℝ ⟶ ℝ ❘ # - 1 prec 32 ❘ = minus_real_lit ❙
axiom_realMinusIsRatMinus : {x : ℚ} ⊦ arithmetics?RealArithmetics?uminus x ≐ arithmetics?RationalArithmetics?uminus x ❙
/T Addition ❙
addition : ℝ ⟶ ℝ ⟶ ℝ ❘ # 1 + 2 prec 12 ❘ = plus_real_lit ❙
axiom_realPlusIsRatPlus : {x : ℚ, y : ℚ} ⊦ arithmetics?RealArithmetics?addition x y ≐ arithmetics?RationalArithmetics?addition x y ❙
axiom_plusUminus : {x : ℝ} ⊦ (x + (-x)) ≐ 0 ❙
/T Subtraction ❙
subtraction : ℝ ⟶ ℝ ⟶ ℝ ❘ = [a,b] a + (-b) ❘ # 1 - 2 prec 12 ❙
/T Multiplication ❙
multiplication : ℝ ⟶ ℝ ⟶ ℝ ❘ # 1 ⋅ 2 prec 22 ❘ = times_real_lit ❙
axiom_realTimesIsRatTimes : {x : ℚ, y : ℚ} ⊦ arithmetics?RealArithmetics?multiplication x y ≐ arithmetics?RationalArithmetics?multiplication x y ❙
/T Division ❙
no_zero_reals = ⟨ x : ℝ | ⊦ x ≠ 0 ⟩ ❘ # ℝ* ❙
inverse : {x:ℝ, p:⊦ x ≠ 0} ℝ ❘ # inv 1 %I2 prec 32 ❙
inverseTyped : ℝ* ⟶ ℝ* ❘ # inverseTyped 1 prec -1 ❙
axiom_inv : {x : ℝ, p : ⊦ x ≠ 0} ⊦ x ⋅ (inv x) ≐ 1 ❙
axiom_inv2 : {r : ℝ* } ⊦ r ⋅ (inverseTyped r) ≐ 1 ❘ # axiom_inv2 ❙
div : {r:ℝ,s:ℝ, p:⊦ s ≠ 0} ℝ ❘ = [r,s,p] r ⋅ (inv s) ❘ # 1 / 2 %I3 prec 5 ❙
/T Exponentiation ❙
exponentiation : ℝ ⟶ ℝ ⟶ ℝ ❘ # 1 ^ 2 prec 32 ❙
axiom_realExpIsRatExp: {x : ℚ, y : ℚ} ⊦ arithmetics?RealArithmetics?exponentiation x y ≐ arithmetics?RationalArithmetics?exponentiation x y ❙
/T Roots ❙
root : {n : ℝ, m : ℕ, p : ⊦ ∃![x] x^m ≐ n}ℝ ❘ = [n,m,p] ι [x] x^m ≐ n ❘ # 2 √ 1 %I3 prec 32 ❙
squareRoot : {n : ℝ, p : ⊦ ∃![m] m^2 ≐ n}ℝ ❘ = [n,p] 2 √ n ❘ # √ 1 %I2 prec 32 ❙
/T Order ❙
leq : ℝ ⟶ ℝ ⟶ bool ❘ # 1 ≤ 2 prec 102 ❙
geq : ℝ ⟶ ℝ ⟶ bool ❘ = [n,m] m ≤ n ❘ # 1 ≥ 2 prec 102 ❙
lessthan : ℝ ⟶ ℝ ⟶ bool ❘ = [n,m] n ≤ m ∧ n ≠ m ❘ # 1 < 2 prec 102 ❙
morethan : ℝ ⟶ ℝ ⟶ bool ❘ = [n,m] n ≥ m ∧ n ≠ m ❘ # 1 > 2 prec 102 ❙
max : ℝ ⟶ ℝ ⟶ ℝ ❘ # max 1 2 ❙
min : ℝ ⟶ ℝ ⟶ ℝ ❘ # min 1 2 ❙
axiom_realLeqIsRatLeq : {x : ℚ, y : ℚ} ⊦ arithmetics?RealArithmetics?leq x y ≐ arithmetics?RationalArithmetics?leq x y ❙
/T Subtypes ❙
NonNegativeRealNumbers : type ❘ # ℝ^+ ❘ = ⟨ x : ℝ | ⊦ x ≥ 0 ⟩❙
PositiveRealNumbers : type ❘ # ℝ+ ❘ = ⟨ x : ℝ | ⊦ x > 0 ⟩❙
/T Suprema ❙
// to allow for later usage of subspaces by way of a boolean function that tells whether it is part of the domain or not ❙
predAsSub : (ℝ ⟶ bool) ⟶ type ❘ = [P] ⟨ z : ℝ | ⊦ P z ⟩ ❘ # pred 1 ❙
sup : (ℝ ⟶ bool) ⟶ ℝ ❙
axiom_sup1 : {P : ℝ ⟶ bool, y : pred P} ⊦ y ≤ sup P ❙
axiom_sup2 : {P : ℝ ⟶ bool, y : ℝ, p : {z: pred P}⊦z ≤ y} ⊦ sup P ≤ y ❙
/T Others ❙
absolute : ℝ ⟶ ℝ^+ ❘ // = [q] case q < 0 ⟹ -q . q ❘ # | 1 | prec 8 ❙
/T Field Axioms ❙
axiom_associativePlus : {x: ℝ,y,z} ⊦ x + (y + z) ≐ (x + y) + z ❘ # associative_plus_real 1 2 3❙
axiom_associativeTimes : {x: ℝ,y,z} ⊦ x ⋅ (y ⋅ z) ≐ (x ⋅ y) ⋅ z ❘ # associative_times_real 1 2 3 ❙
axiom_leftUnitalPlus : {x : ℝ} ⊦ 0 + x ≐ x ❘ # leftunital_plus_real 1 ❙
axiom_rightUnitalPlus : {x : ℝ} ⊦ x + 0 ≐ x ❘ # rightunital_plus_real 1❙
axiom_leftUnitalTimes : {x : ℝ} ⊦ 1 ⋅ x ≐ x ❘ # leftunital_times_real 1 ❙
axiom_rightUnitalTimes : {x : ℝ} ⊦ x ⋅ 1 ≐ x ❘ # rightunital_times_real 1 ❙
axiom_distributive : {x : ℝ, y, z} ⊦ x ⋅ (y + z) ≐ (x ⋅ y) + (x ⋅ z) ❘ # distributive_real 1 2 3 ❙
axiom_commutativePlus : {x : ℝ,y} ⊦ x + y ≐ y + x ❘ # addition_commutative_real 1 2 ❙
axiom_commutativeTimes : {x : ℝ,y} ⊦ x ⋅ y ≐ y ⋅ x ❘ # times_commutative_real 1 2 ❙
❚
theory ExtendedReals : base:?Logic =
include ?RealArithmetics ❙
// extended_reals : type ❘ # ℝ∞ ❙
// reals_are_extended : ℝ <* ℝ∞ ❙
infty : ℝ ❘ # ∞ prec 1 ❙
// leq : ℝ∞ ⟶ ℝ∞ ⟶ bool ❘ # 1 ≤ 2 prec 101 ❙
// TODO neginfty : ℝ∞ ❘ = - ∞ ❘ # -∞ ❙
❚