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 : ℝ∞ ❘ = - ∞ ❘ # -∞ ❙