Commit a8926ce5 authored by Sven Wille's avatar Sven Wille

tarski grothendieck

parent 09777e98
......@@ -51,4 +51,12 @@ theory Set_Lemmata : fnd:?Logic =
lemma_union_non_empty2 : {A,B} ⊦ nonempty A ⟶ ⊦ nonempty (B ∪ A) ❙
corollary_empty_set_is_empty : ⊦ empty ∅ ❙
lemma_singleton_in_set : {a, X} ⊦ singleton a ⊆‍ X ⇔ a ∈ X❙
lemma_subset_singleton : {Y, x} ⊦ Y ⊆‍ singleton x ⇔ Y ≐ singleton x ∨ Y ≐ ∅❙
lemma_power_empty : ⊦ ℘ ∅ ≐ singleton ∅ ❙
lemma_empty_union : ⊦ ⋃ ∅ ≐ ∅ ❙
namespace http://mathhub.info/MitM/smglom/other_foundations/mmt_tg ❚
import fnd http://mathhub.info/MitM/Foundation ❚
theory Pairs : fnd:?Logic =
include ?ZF_Base ❙
tuple = opair ❙
pair = tuple ❙
triple : set ⟶ set ⟶ set ⟶ set ❘= [a,b,c] tuple (tuple a b) c ❙
projl : set ⟶ set ❙
projl_def : {a , b} ⊦ projl (pair a b ) ≐ a ❙
projr : set ⟶ set ❙
projr_def : {a,b} ⊦ projr (pair a b ) ≐ b ❙
cartesian_product : set ⟶ set ⟶ set ❘ = [A,B] ⟪ ℘ (℘ (A ∪ B)) | ([x] ∃ [a] ∃ [b] a ∈ A ∧ b ∈ B ∧ x ≐ opair a b ) ⟫ ❘ # 1 × 2 ❙
ternary_product : set ⟶ set ⟶ set ⟶ set ❘= [A,B,C] ((A × B ) × C)❙
quarternary_product : set ⟶ set ⟶ set ⟶ set ⟶ set ❘ = [A,B,C,D] (((A × B) × C) × D)❙
theory Paris_theorems : fnd:?Logic =
include ?Pairs ❙
lemma_equal_pairs : {A , B , C , D} ⊦ pair A B ≐ pair C D ⟶ ⊦ A ≐ C ∧ B ≐ D ❙
lemma_pair_id : {a, b, c} ⊦ a ≐ pair b c ⟶ ⊦ pair (projl a) (projr a) ≐ a ❙
lemma_pair_id2 : {a, b, c , d } ⊦ a ∈ (c × d) ⟶ ⊦ b ∈ (c × d ) ⟶ ⊦ projl a ≐ projl b ⟶ ⊦ projr b ≐ projr b ⟶ ⊦ a ≐ b ❙
namespace http://mathhub.info/MitM/smglom/other_foundations/mmt_tg ❚
import fnd http://mathhub.info/MitM/Foundation ❚
theory Relations : fnd:?Logic =
include ?ZF_Base ❙
binary_relation : set ⟶ set ⟶ set ❘ = [a,b] ❙
theory Relations_theorems : fnd:?Logic =
include ?Relations ❙
\ No newline at end of file
......@@ -52,10 +52,13 @@ theory Pairing : fnd:?Logic =
theorem_pair_unique : ⊦ ∀[X] ∀ [Y] ∃! [Z] (X ∈ Z ∧ Y ∈ Z) ❙ // by axiom of extensionality❙
theorem_pair_unique_alt : {X: set} {Y :set } ⊦ ∃! [Z] (X ∈ Z ∧ Y ∈ Z) ❘ # theorem_pair_unique_alt 1 2 ❘ = [X,Y] forallE (forallE theorem_pair_unique X) Y ❙ // by axiom of extensionality❙
upair : set ⟶ set ⟶ set ❘ = [A :set][B : set] that set ([Z] (A ∈ Z ∧ B ∈ Z)) (theorem_pair_unique_alt A B) ❙
upair : set ⟶ set ⟶ set ❘ = [A :set][B : set] that set ([Z] (A ∈ Z ∧ B ∈ Z)) (theorem_pair_unique_alt A B) ❙ // unordered pair ❙
singleton : set ⟶ set ❘ = [A : set] upair A A ❙
opair : set ⟶ set ⟶ set ❘ = [a ,b ] upair (singleton a) (upair a b) ❙ // ordered pair ❙
......
Xboole_0 : are_c=-comparable
XBOOLE_0:5
\ No newline at end of file
XBOOLE_0:5
TARSKI:3
\ No newline at end of file
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