update

source/calculus/sequencesconvergence.mmt

@@ -55,8 +55,8 @@ theory SequenceConvergence : base:?Logic =
 		= [G,a,l] ∀[ε : ℝ+] ∀[N : ℕ] ∃[n : ℕ] (n ≥ N) ∧ ((d (a n) l) < ε) ❙
 	prop_hasLimit : {G: metricSpace} G^ω ⟶ prop  ❘
 		= [G,a] ∃![g] prop_isLimit G a g    ❙
-	limit : {G : metricSpace, a : G^ω, p : ⊦ prop_convergent G a} dom G ❘
-		= [G, a, p] that (dom G) ([g : dom G] prop_converges G a g) p ❘
+	limit : {G : metricSpace, a : G^ω, p : ⊦ prop_convergent G a} G.universe ❘
+		= [G, a, p] that (G.universe) ([g : G.universe] prop_converges G a g) p ❘
 		# lim 2 %I3 ❙
 ❚
     	      

source/measures/measures.mmt

@@ -37,7 +37,7 @@ theory Measure : base:?Logic =
 	measureSpace = {'
   		universe : type ,
   		sigma_algebra : sigmaAlgebra universe ,
-  		measure : measure universe sigma_algebra
+  		rmeasure : measure universe sigma_algebra
 	'}❙
 ❚
 

source/sets/typed_sets.mmt

@@ -138,7 +138,7 @@ theory AllSets : base:?Logic =
 	include ?SetStructures ❙
 	include ?SetRelations ❙
 
-	typeof : {A} set A ⟶ type ❘ // = [A,s] ⟨A | ([x] ⊦ x ∈ s)⟩ ❘ # setastype 2 ❙
+	typeof : {A} set A ⟶ type ❘// = [A,s] ⟨ x : A | ⊦ x ∈ s⟩ ❘ # setastype 2 ❙
 	elemof : {A}{s : set A, e : A} ⊦ e ∈ s ⟶ setastype s ❘ # elem 2 3 %I4❙
 ❚