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

import base http://mathhub.info/MitM/Foundation 
import sets http://mathhub.info/MitM/core/typedsets 
import algebra http://mathhub.info/MitM/core/algebra 
import topo http://mathhub.info/MitM/core/topology 

theory MetricSpace : base:?Logic = 
   include arithmetics?RealArithmetics 
   include ☞sets:?SetStructures 
   
	theory signature_theory : base:?Logic =
		include ☞sets:?SetStructures/setstruct_theory 
		d : U ⟶ U ⟶ ℝ 
	
	signature = Mod ☞?MetricSpace/signature_theory 
   
	prop_nonNegative :  {G : type, d : G ⟶ G ⟶ ℝ} prop  = [G,d] ∀[x]∀[y] 0 ≤ d x y  
	prop_identityOfIndiscernibles :  {G : type, d : G ⟶ G ⟶ ℝ} prop  = [G,d] ∀[x]∀[y] d x y ≐ 0 ⇒ x ≐ y     
	prop_positiveDefinite : {G : type, d : G ⟶ G ⟶ ℝ^+ }prop  = [G,d] prop_nonNegative G d ∧ prop_identityOfIndiscernibles G d 
	prop_symmetric :  {G : type, d : G ⟶ G ⟶ ℝ} prop 
		= [G][d] ∀[x]∀[y]  d x y  ≐ d y x  
		
	prop_pseudoMetric : {G : type, d : G ⟶ G ⟶ ℝ^+} prop  = [G,d] prop_positiveDefinite G d ∧ prop_symmetric G d 
		
	theory pseudoMetricSpace_theory : base:?Logic =
		include ☞sets:?SetStructures/setstruct_theory 
		d : U ⟶ U ⟶ ℝ^+ 
		axiom_isPseudoMetric : ⊦ prop_pseudoMetric U d 
	
	pseudoMetricSpace = Mod ☞?MetricSpace/pseudoMetricSpace_theory 
	
	prop_triangleInequality :  {G : type, d : G ⟶ G ⟶ ℝ} prop 
		= [G][d] ∀[x]∀[y]∀[z] (d x z)  ≤ ((d y x) + (d y z))  

	theory metricSpace_theory : base:?Logic =
		include ?MetricSpace/pseudoMetricSpace_theory 
		axiom_triangleInequality : ⊦ prop_triangleInequality U d 
	
	metricSpace = Mod ☞?MetricSpace/metricSpace_theory 
	// metricSpace : type ⟶ type  ❘ # metricSpace 1 ❙ // = [A] ⟨metricspace | ([G] ⊦ A ≐≐ G.universe)⟩❘
  
	distanceFunction : type ⟶ type ❘ = ⟨A ⟶ A ⟶ ℝ | ([x] ⊦ ∃[G: metricSpace] x ≐ G.d)⟩ ❘ # distanceFunction 1 ❙ 
	metric : {G: metricSpace} (G.universe ⟶ G.universe ⟶ ℝ)  # d 2 3  = [G][a][b] (G.d) a b 


theory MetricMonoid : base:?Logic =
	include ?MetricSpace 
	include algebra?Monoid
	
	theory metricMonoid_theory : base:?Logic =
		include algebra?Monoid/monoid_theory 
		include ?MetricSpace/metricSpace_theory 
	
	metricMonoid = Mod ☞?MetricMonoid/metricMonoid_theory 


theory Ball : base:?Logic = 
   include ?MetricSpace 
   include ☞sets:?AllSets 
   openBall : {M: metricSpace} M.universe ⟶ ℝ ⟶ set (M.universe) 
   = [M][a][ε] ⟪ (doms M) | ([x] (d x a) < ε) ⟫  # B_ 3 2
   closedBall : {M: metricSpace} M.universe ⟶ ℝ ⟶ set (M.universe) 
   = [M][a][ε] ⟪ (doms M) | ([x] (d x a) ≤ ε) ⟫  // MiKo: how to do \overline{B} in the notation? ❙


theory MetricSpaceAsTopology : base:?Logic =
	include ?Ball 
	include ☞topo:?HausdorffTopology 
	// Why only Hausdorff? Don't we obtain even stronger conditions (normal?)? ❙
	// A: as soon as we formalized those, sure :) ❙
	openColl : {M : metricSpace} set (set (dom M)) 
	axiom_ballIsOpen : {M : metricSpace, a : M.universe, ε : ℝ} ⊦ (openBall M a ε) ∈ (openColl M) 
	
	axiom_emptyIsOpen : {M : metricSpace} ⊦ prop_emptyInColl (openColl M)  # emptyisopen 1 
	axiom_fullIsOpen : {M : metricSpace} ⊦ prop_fullInColl (openColl M)  # fullisopen 1 
	axiom_unionIsOpen : {M : metricSpace} ⊦ prop_unionInColl (openColl M)  # unionisopen 1 
	axiom_intersectionIsOpen : {M : metricSpace} ⊦ prop_finiteIntersection (openColl M)  # intersectionisopen 1 
	
	axiom_metricIsHausdorff : {M : metricSpace} ⊦ hausdorffProperty (dom M) (openColl M)  # miHaus 1 
	metricAsTopology : {M : metricSpace}hausdorffTopology (dom M)  
		= [M] [' 
			universe := M.universe, 
			d := M.d,
			axiom_isPseudoMetric := M.axiom_isPseudoMetric,
			axiom_triangleInequality := M.axiom_triangleInequality,
			coll := openColl M,
			axiom_empty := axiom_emptyIsOpen M,
			axiom_full := axiom_fullIsOpen M,
			☞?OML?axiom_union := axiom_unionIsOpen M,
			axiom_intersection := axiom_intersectionIsOpen M,
			ishausdorff := miHaus M
		'] 

  
theory RealMetricSpace : base:?Logic =
   include arithmetics?RealArithmetics 
   include ?MetricSpace 
   
   realmetric : ℝ ⟶ ℝ ⟶ ℝ^+  = [a,b] | a - b |  # ds 1 , 2 
   axiom_realIsPseudoMetric : ⊦ prop_pseudoMetric ℝ realmetric 
   axiom_triangleReal : ⊦ prop_triangleInequality ℝ realmetric 

   realmetricspace : metricSpace 
   		= [' 
   			universe := ℝ, 
   			d := realmetric, 
   			axiom_isPseudoMetric := axiom_realIsPseudoMetric,
   			axiom_triangleInequality := axiom_triangleReal
   		']  # ℝm    
   		
   	
   axiom_predRealIsPseudoMetric : {P : ℝ ⟶ bool} ⊦ prop_pseudoMetric (pred P) realmetric   # pseudom 1 
   axiom_predTriangle : {P : ℝ ⟶ bool} ⊦ prop_triangleInequality (pred P) realmetric  # realmet 1 
   
   realSubMetric : {P : ℝ ⟶ bool} metricSpace 
   		= [P] [' 
   			universe := pred P, 
   			d := [a : pred P][b : pred P] realmetric a b,
   			axiom_isPseudoMetric := pseudom P,
   			axiom_triangleInequality := realmet P
   		']  # mpred 1 
   		
   axiom_mpredIsSuptype : {P : ℝ ⟶ bool} (mpred P).universe <* ℝ