Commit 5dc6c4ff authored by Sven Wille's avatar Sven Wille

mehr zftrash

parent b8a58821
......@@ -7,9 +7,11 @@ import fnd http://mathhub.info/MitM/Foundation ❚
theory Set_Operations : fnd:?Logic =
include http://mathhub.info/MitM/smglom/other_foundations/mmt_tg?ZF_Base ❙
bigintersection : set ⟶ set ❘ = [S] ⟪ (⋃ S) | ([x] ∀ [Z] (Z ∈ S ⇒ x ∈ Z)) ⟫ ❘ # ⋂ 1
bigintersection : {S : set} ⊦ (∃ [x : set] (x ∈ S)) ⟶ set ❘ = [S,h] ⟪ (⋃ S) | ([x] ∀ [Z] (Z ∈ S ⇒ x ∈ Z)) ⟫ ❘ # ⋂ 1 2 ❙ // the intersection of the empty set is undefined
binaryIntersection : set ⟶ set ⟶ set ❘ = [A , B] ⋂ upair A B ❘ # 1 ∩ 2 prec 10 ❙
upairNotEmpty : ⊦ ∀[a] ∀ [b] ∃[x] x ∈ upair a b ❙
binaryIntersection : set ⟶ set ⟶ set ❘ = [A , B] ⋂ (upair A B) (forallE (forallE upairNotEmpty A) B) ❘ # 1 ∩ 2 prec 10 ❙
set_complement : set ⟶ set ⟶ set ❘= [A,B] ⟪ A | ([x] ¬ (x ∈ B)) ⟫ ❘# 1 \ 2 ❙
......@@ -21,6 +23,7 @@ theory Set_Operations : fnd:?Logic =
succ : set ⟶ set ❘ = [a] cons a a ❙
theory Set_Properties : fnd:?Logic =
......@@ -43,7 +46,7 @@ theory Set_Properties : fnd:?Logic =
ball : set ⟶ (set ⟶ prop) ⟶ prop ❘ = [s , p ] ∀ [x] x ∈ s ⇒ p s ❙
bex : set ⟶ (set ⟶ prop) ⟶ prop ❘ = [s , p] ∃[x] x ∈ s p s ❙
bex : set ⟶ (set ⟶ prop) ⟶ prop ❘ = [s , p] ∃[x] x ∈ s p s ❙
......
namespace http://mathhub.info/MitM/smglom/other_foundations/mmt_tg ❚
import fnd http://mathhub.info/MitM/Foundation ❚
theory BoolZF : fnd:?Logic =
include http://mathhub.info/MitM/smglom/other_foundations/mmt_tg?Set_Operations❙
zero = ∅ ❘# ff ❙
one = singleton ∅ ❘# tt❙
two = succ one ❙
boolSet : set ❘ = two ❙
cond = [c,a,b : set] if (c ≐ tt) then a else b ❙
notzf = [b] cond b ff tt ❙
andzf = [a,b] cond a b ff❙
orzf = [a,b] cond a tt b❙
xor = [a,b] cond (orzf (andzf a b) (andzf (notzf a) (notzf b))) ff tt❙
boolToboolzf = [b] if b then tt else ff ❙
\ No newline at end of file
......@@ -35,6 +35,9 @@ theory PairsTG : fnd:?Logic =
lefts : set ⟶ set ❘ = [s] ⟪ ⋃ ⋃ s | ([x] ∃[y] tuple x y ∈ s) ⟫ ❙
rights : set ⟶ set ❘ = [s] ⟪ ⋃ ⋃ s | ([x] ∃ [y] tuple y x ∈ s) ⟫ ❙
split : set ⟶ (set ⟶ set ⟶set) ⟶ set ❘ = [p,f] f (projl p) (projr p) ❙
theory Paris_theorems : fnd:?Logic =
......
......@@ -39,11 +39,20 @@ theory Relations : fnd:?Logic =
theory Abstractions : fnd:?Logic =
// include ?Relatioins ❙
// Lambda = [A,b] ❙
include ?Relations ❙
include http://mathhub.info/MitM/smglom/other_foundations/mmt_tg?ReplacementFunction ❙
Lambda = [A,b] replaceFn A ([x] opair x (b x)) ❙
apply = [f,xs] ⋃ (image f xs)❙
Pii = [X,Y] ⟪ ℘ (Sigma X Y) | ([f] X ⊆‍ (domain f) ∧ is_function f) ⟫ ❙ // the name Pi is already used by lf ❙
function_space = [A,B] Pii A ([x : set] B ) ❙
theory Relations_theorems : fnd:?Logic =
// include ?Relations ❙
include ?Relations ❙
theorem_cantor : ⊦ ∀ [A] ∀ [b] ∃ [S] S ∈ ℘ A ⇒ ∀ [x] x ∈ A ⇒ b x ≠ S❙
\ No newline at end of file
namespace http://mathhub.info/MitM/smglom/other_foundations/mmt_tg ❚
import fnd http://mathhub.info/MitM/Foundation ❚
// an interpretation of the sum type in zfc set theory ❚
theory SumType : fnd:?Logic =
include http://mathhub.info/MitM/smglom/other_foundations/mmt_tg?PairsTG ❙
include http://mathhub.info/MitM/smglom/other_foundations/mmt_tg?BoolZF ❙
sumType = [a,b] (ff × a) ∪ (tt × b) ❘ # sumSet ❙
Inl = [v] opair ff v ❙
Inr = [v] opair tt v ❙
case = [a,b] ❙
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment