namespace http://mathhub.info/MitM/core/calculus ❚

import top http://mathhub.info/MitM/core ❚
import base http://mathhub.info/MitM/Foundation ❚

import meta http://cds.omdoc.org/mmt ❚

//   author: Theresa Pollinger ❚
 
 
//   a lot of stuff here stolen from dgls.mmt xx: 
//   To not make things too awful, I've now fixed one ⋁ for a vectorspace; just for notational reasons. ❚

//   as "domains" is overloaded between disciplines: in numerical modeling, we are talking about finite, (singly) connected subspaces of ℝ^n as domains ❚

theory Intervals : base:?Logic = 
	include ☞top:/arithmetics?RealArithmetics ❙
	include ☞top:/algebra?RealField ❙
	include ?RealMetricSpace ❙

	theory interval_theory : base:?Logic =
		left : ℝ ❙
		right : ℝ ❙
		leftPred : ℝ ⟶ ℝ ⟶ prop ❙
		rightPred : ℝ ⟶ ℝ ⟶ prop ❙
		predicate : ℝ ⟶ prop ❘ = [x] leftPred left x ∧ rightPred x right ❙
		tp : type ❘ = pred predicate ❙ 
	❚
	
	interval : type ❘ = Mod ☞?Intervals/interval_theory ❙
	
	closedInterval : ℝ ⟶ ℝ ⟶ interval ❘ = [a,b] ['
		left := a,
		right := b,
		leftPred := ([x,y] x ≤ y),
		rightPred := ([x,y] x ≤ y)
	'] ❘ # [ 1 ; 2 ] ❙
	
❚

theory OneCuboid : base:?Logic = 
	include ☞top:/arithmetics?RealArithmetics ❙

	theory oneCuboid_theory : base:?Logic =
		left : ℝ ❙
		right : ℝ ❙
		leftPred : ℝ ⟶ ℝ ⟶ prop ❙
		rightPred : ℝ ⟶ ℝ ⟶ prop ❙
		predicate : ℝ ⟶ prop ❘ = [x] leftPred left x ∧ rightPred x right ❙
		tp : type ❘ = pred predicate ❙ 
	❚
	
	interval : type ❘ = Mod ☞?Intervals/interval_theory ❙
	
	closed1Cuboid : ℝ ⟶ ℝ ⟶ interval ❘ = [a,b] ['
		left := a,
		right := b,
		leftPred := ([x,y] x ≤ y),
		rightPred := ([x,y] x ≤ y)
	'] ❘ # [ 1 ; 2 ] ❙
	
❚

theory GeneralDomains : base:?Logic = 
  include ☞top:/arithmetics?NaturalNumbers ❙
  include ☞top:/algebra?RealField ❙
  include ?Ball ❙
  include ☞top:/algebra?Vectorspace ❙
  
  theory generalDomain_theory : base:?Logic =
  	 include ☞top:/algebra?Vectorspace/vectorspace_theory (realField) ❙
  	 include ?MetricSpace/metricSpace_theory ❙
  	 dimension : ℕ ❙
  	 domainPred : U ⟶ prop ❙
  	 domain : type ❘ = ⟨ x : U | ⊦ domainPred x ⟩ ❙
  	 boundaryPred1 : U ⟶ prop ❘ = [b] ∀ [ε : ℝ+] ∃[x : domain] d x b < ε ❙
  	 boundaryPred2 : U ⟶ prop ❘ = [b] ∀ [ε : ℝ+] ∃[x : U] d x b < ε ∧ ¬ domainPred x ❙
  	 boundaryPred : U ⟶ prop ❘ = [b] boundaryPred1 b ∧ boundaryPred2 b ❙
  	 boundary : type  ❘ = ⟨ x : U | ⊦ boundaryPred x ⟩ ❙
  ❚
  	 
  generalDomain = Mod ☞?GeneralDomains/generalDomain_theory ❙
❚  

// view IntervalsAsDomains : ?GeneralDomains/generalDomain_theory ⟶ ?Intervals/interval_theory =
    = ℝ ❙ 
   // Dimension = 1 ❙
   DomainPred = interval_pred ❙
   BoundaryPred = boundary_pred ❙
   // vec_pred_as_sub = pred_as_sub ❙
❚