update

source/math.mmt

@@ -222,6 +222,7 @@ theory InformalProofs : ur:?LF =
 	proofsketch : {A : prop} string ⟶ ⊦ A ❘ # sketch 2 ❙
 	byproof : {A,B} ⊦ A ⟶ ⊦ B ❘ # by 3 ❙
 	addproofstep : {A,B,C: prop} ⊦ A ⟶ ⊦ B ⟶ ⊦ B ❘ # 4 and 5 ❙
+	trivial : {A : prop} ⊦ A ❘ = [A] sketch "trivial" ❘ # trivial %I1 ❙
 ❚
 
 
@@ -294,7 +295,9 @@ theory ProductTypes : http://gl.mathhub.info/MMT/LFX/Sigma?LFSigma =
 	// to have it in the meta-theory ❙                       
 ❚
 theory FiniteTypes : http://gl.mathhub.info/MMT/LFX/Finite?LFFinite = ❚
-theory InductiveTypes : http://gl.mathhub.info/MMT/LFX/WTypes?Inductive = ❚
+theory InductiveTypes : http://gl.mathhub.info/MMT/LFX/WTypes?Inductive =
+    include ?Logic ❙
+❚
 
 theory Sequences =
 	// Ditto ❙

source/sets/zf.mmt

@@ -37,6 +37,12 @@ theory Separation : fnd:?Logic =
 	sep_constructor : {s : set,P : set ⟶ prop}set ❘ = [s,P] that set ([x] ∀[e]e ∈ x ⇔ (e ∈ s ∧ P e)) (axiom_separation P s)❘ # ⟪ 1 | 2 ⟫ prec -1 ❙
 ❚
 
+theory Intersection : fnd:?Logic =
+    include ?Separation ❙
+
+    intersect : set ⟶ set ⟶ set ❘ = [s,t] ⟪ s | ([x] x ∈ t) ⟫ ❘ # 1 ∩ 2 ❙
+❚
+
 theory Regularity : fnd:?Logic =
 	include ?Sets ❙
 	
@@ -115,7 +121,7 @@ theory Replacement : fnd:?Logic =
 	include fnd:?DescriptionOperator ❙
 	
 	axiom_replacement : {a,f} ⊦ prop_replacement a f ❘ # axiom_replacement 1 2❙
-	replacement : set ⟶ (set ⟶ set) ⟶ set ❘ = [A,f] that set ([B] ∀[z] (z ∈ B ⇔ ∃[a] a ∈ A ∧ z ≐ f a)) (axiom_replacement A f) ❘ # Im 2 of 1 ❙
+	replacement : set ⟶ (set ⟶ set) ⟶ set ❘ = [A,f] that set ([B] ∀[z] (z ∈ B ⇔ ∃[a] a ∈ A ∧ z ≐ f a)) (axiom_replacement A f) ❘ # Img 2 of 1 ❙
 ❚
 
 theory Infinity : fnd:?Logic =
@@ -156,6 +162,7 @@ theory Finite : fnd:?Logic =
 theory ZF : fnd:?Logic =
     include ?ZFBase ❙
     include ?Finite ❙
+    include ?Intersection ❙
 
 	setdiff : set ⟶ set ⟶ set ❘= [A,B] ⟪ A | ([x] ¬ x ∈ B) ⟫ ❘ # 1 \ 2 ❙
 	subtract : set ⟶ set ⟶ set ❘= [A,a] A \ (singleton a) ❘ # 2 - 3 ❙