Commit 01f8522f by Sven Wille

### stuffy

parent a8926ce5
 ... ... @@ -33,8 +33,11 @@ theory FinSeqFunctions : base:?InductiveTypes = finiteSequenceMap : {A : type} {B : type} {n : ℕ} finSeq n A ⟶ (A ⟶ B) ⟶ finSeq n B ❘= [A , B , n , fn , mp] [a ,b ,c] mp (fn a b c) ❘ # finSeqMap 4 5 ❙ incIf : {A : type} {b : type} ℕ ⟶ ℕ ⟶ ( ℕ ⟶ A) ⟶ A❙ // helper for finiteSequenceFoldLeft ❙ finiteSequenceFoldLeftLoop : {A : type}{B : type}{n : ℕ}{m : ℕ} (A ⟶ B ⟶ A) ⟶ A ⟶ finSeq n B ⟶ A ❘ = [A , B , n , m , f , start , fs] if ❙ finiteSequenceFoldLeftLoop : {A : type}{B : type}{n : ℕ}{m : ℕ} (A ⟶ B ⟶ A) ⟶ A ⟶ finSeq n B ⟶ A ❘ = [A , B , n , m , f , start , fs] incIf ❙ finiteSequenceFoldLeft : {A : type}{B : type} {n : ℕ} (A ⟶ B ⟶ A) ⟶ A ⟶ finSeq n B ⟶ A ❘ # finSeqFoldL 1 2 3 4 5 6 ❙ finiteSequenceFoldLeftBZ : {A : type}{B : type}{f : A ⟶ B ⟶ A}{start : A}{fs : finSeq 0 B} ⊦ finiteSequenceFoldLeft A B 0 f start fs ≐ start❙ ... ...
 namespace http://mathhub.info/MitM/smglom/other_foundations/mmt_sear ❚ import fnd http://mathhub.info/MitM/Foundation ❚ theory pre_axioms : fnd:?Logic = element : type ❙ set : type ❙ typing : type ❙ rel : set ⟶ set ⟶ typing ❙ element_of : element ⟶ set ⟶ typing ❘ # 1 ∈ 2 ❙ ❚
 ... ... @@ -16,6 +16,8 @@ theory Set_Operations : fnd:?Logic = symmetric_difference : set ⟶ set ⟶ set ❘= [A,B] (A \ B) ∪ (B \ A) ❘ # 1 Δ 2 ❙ complement : {a : set } {b : set} ⊦ a ⊆‍ b ⟶ set ❘ = [a,b,h] b \ a ❙ ❚ theory Set_Properties : fnd:?Logic = ... ... @@ -35,6 +37,7 @@ theory Set_Properties : fnd:?Logic = nonempty : set ⟶ prop ❘ = [A] ∃ [x] x ∈ A ❙ empty : set ⟶ prop ❘ = [A] ¬ ∃ [x] x ∈ A ❙ ❚ theory Set_Lemmata : fnd:?Logic = ... ...
 namespace http://mathhub.info/MitM/smglom/other_foundations/mmt_tg ❚ import fnd http://mathhub.info/MitM/Foundation ❚ theory FunctionsTG : fnd:?Logic = ❚
 namespace http://mathhub.info/MitM/smglom/other_foundations/mmt_tg ❚ import fnd http://mathhub.info/MitM/Foundation ❚ theory LFFN : fnd:?Logic = set : type ❙ tpl : set ⟶ set ⟶ tplT A B❙ ttpl : {a : set }{b : set} ⊦ a ∈ b ⟶ tpl a b ❘ # ⟦ 1 , 2 ⟧ ❙ ❚
 ... ... @@ -2,30 +2,46 @@ namespace http://mathhub.info/MitM/smglom/other_foundations/mmt_tg ❚ import fnd http://mathhub.info/MitM/Foundation ❚ theory Pairs : fnd:?Logic = theory PairsTG : fnd:?Logic = include ?ZF_Base ❙ tuple = opair ❙ pair = tuple ❙ is_opair : set ⟶ prop ❘ = [s] ∃ [a] ∃ [b] s ≐ opair a b ❙ 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 prec 20 ❙ // proof that the only "constructor" of the cartesian product is an opair (i.e. the shape of all elements that are in the cartesian product are opairs)❙ cartesian_product : set ⟶ set ⟶ set ❘ = [A,B] ⟪ ℘ (℘ (A ∪ B)) | ([x] ∃ [a] ∃ [b] a ∈ A ∧ b ∈ B ∧ x ≐ opair a b ) ⟫ ❘ # 1 × 2 ❙ constructor_cartesian_product : ∀ [x] x ∈ cartesian_product ❙ 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)❙ lemma_pair_in_cartesian_product : {A , B} {a ,b} ⊦ a ∈ A ⟶ ⊦ b ∈ B ⟶ ⊦ pair ∈ a × b ❙ projl : {b}{c} {a : set} ⊦ a ∈ b × c ⟶ set ❙ projl_def : {a , b} {A,B} ⊦ projl A B (pair a b ) (lemma_pair_in_cartesian_product A B a b) ≐ a ❙ projr : {b}{c} {a : set } ⊦ a ∈ set ⟶ set ❙ projr_def : {a,b} ⊦ projr (pair a b ) ≐ b ❙ lefts : set ⟶ set ❙ lefts_def : {s : set} {D : set }{ C : set } {h : ⊦ s ∈ D × C } ⊦ lefts s ≐ ⟪ D | ([x] ∃ [y] opair x y ∈ s ) ⟫ ❙ rights : set ⟶ set ❙ rights_def : {s : set} {D : set }{ C : set } {h : ⊦ s ∈ D × C } ⊦ rights s ≐ ⟪ C | ([x] ∃ [y] opair y x ∈ s ) ⟫ ❙ ❚ theory Paris_theorems : fnd:?Logic = include ?Pairs ❙ include ?PairsTG ❙ lemma_equal_pairs : {A , B , C , D} ⊦ pair A B ≐ pair C D ⟶ ⊦ A ≐ C ∧ B ≐ D ❙ ... ... @@ -33,5 +49,5 @@ theory Paris_theorems : fnd:?Logic = lemma_pair_id2 : {a, b, c , d } ⊦ a ∈ (c × d) ⟶ ⊦ b ∈ (c × d ) ⟶ ⊦ projl a ≐ projl b ⟶ ⊦ projr b ≐ projr b ⟶ ⊦ a ≐ b ❙ ❚
 ... ... @@ -3,10 +3,25 @@ namespace http://mathhub.info/MitM/smglom/other_foundations/mmt_tg ❚ import fnd http://mathhub.info/MitM/Foundation ❚ theory Relations : fnd:?Logic = include ?ZF_Base ❙ include ?PairsTG ❙ binary_relation : set ⟶ set ⟶ set ❘ = [a,b] ❙ is_binary_relation_of : set ⟶ set ⟶ set ⟶ prop ❘ = [s,f,t] ∀ [x] (x ∈ s) ⇒ is_opair x ∧ ∃ [a] ∃ [b] (a ∈ f) ∧ (b ∈ t) ∧ projl x ≐ a ∧ projr x ≐ b ❙ relation : set ⟶ set ⟶ set ❘ = [a,b] ℘ (a × b) ❙ // "relation type" ❙ domain = lefts ❙ range = rights ❙ field : set ⟶ set ❙ field_def : {r} {D} {C}{h : ⊦ r ∈ relation D C} ⊦ field r ≐ domain r ∪ range r ❙ converse : set ⟶ set ❙ converse_def : {a : set} {d } {c : set }{h : ⊦ a ∈ relation d c } ⊦ converse a ≐ ⟪ c × d | ([x] opair (projr x )(projl x) ∈ a) ⟫❙ composition : set ⟶ set ⟶ set ❙ // composition_def : {a}{b}{x}{y}{z} {h : ⊦ a ∈ relation x y}{h0 : ⊦ b ∈ relation y z} ⊦ composition a b ≐ ❙ ❚ theory Relations_theorems : fnd:?Logic = ... ...
 namespace http://mathhub.info/MitM/smglom/other_foundations/mmt_tg/TypedTest ❚ import fnd http://mathhub.info/MitM/Foundation ❚ import TG http://mathhub.info/MitM/smglom/other_foundations/mmt_tg❚ theory TT : fnd:?Logic = include TG:?ZF_Base ❙ ❚
 Xboole_0 : are_c=-comparable XBOOLE_0:5 TARSKI:3 \ No newline at end of file TARSKI:3 relat_1:RelExistence \ 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!