Commit d945934b authored by Sven Wille's avatar Sven Wille

intervals and finsequences

parent 9b58c127
......@@ -10,9 +10,6 @@ theory FinSequences : base:?InductiveTypes =
finiteSequence : INat ⟶ type ⟶ type ❘= [n : INat , A] {x : INat} ⊦ leN (Suc Zero) x ⟶ ⊦ (leN x n) ⟶ A ❘# finSeq 1 2 ❙
......@@ -34,3 +31,18 @@ theory FinSeqProps : base:?InductiveTypes =
theory FinSeqFunctions : base:?Logic =
include ?FinSequences ❙
finiteSequenceMap : {A : type} {B : type} {n : INat} finSeq n A ⟶ (A ⟶ B) ⟶ finSeq n B ❘= [A , B , n , fn , mp] [a ,b ,c] mp (fn a b c) ❘ # finSeqMap 4 5 ❙
def finiteSequenceFoldL : (A : type , B : type , fn : A ⟶ B ⟶ A , starValue : A ) ❘ =
finSeqFoldL : {n : INat } ⟶ finSeq n B ⟶ A❙
Zero ❙
theory FinSeqProd : base:?Logic =
finSeqIntervalProd : ❙
......@@ -2,6 +2,10 @@ namespace http://mathhub.info/MitM/smglom/calculus ❚
import top http://mathhub.info/MitM/smglom ❚
import base http://mathhub.info/MitM/Foundation ❚
import ts http://mathhub.info/MitM/smglom/typedsets ❚
import arith http://mathhub.info/MitM/smglom/arithmetics ❚
import fnd http://mathhub.info/MitM/Foundation ❚
import lfx http://gl.mathhub.info/MMT/LFX/Sigma ❚
import meta http://cds.omdoc.org/mmt ❚
......@@ -39,7 +43,13 @@ theory Intervals : base:?Logic =
'] ❘ # [ 1 ; 2 ] ❙
type_closedInterval : ℝ ⟶ ℝ ⟶ type ❘= [l,r] ⟨ iv : interval | ⊦ iv ≐ closedInterval l r⟩ ❘ # cInterval 1 2❙
// type_closedInterval : type ❘= ⟨ iv : interval | ⊦ ∃ [l] ∃[r] iv ≐ closedInterval l r⟩ ❘ # cInterval ❙
// hint : by type_ci having the same fields as interval , it automatically becomes a subtype of interval (and I think also the otherway arround)❙
type_ci : type ❘= {' left : ℝ , right : ℝ , leftPred : ℝ ⟶ ℝ ⟶ prop := ([x,y] x ≤ y) ,
rightPred : ℝ ⟶ ℝ ⟶ prop := ([x,y] x ≤ y) , predicate : ℝ ⟶ prop := [x] leftPred left x ∧ rightPred x right , tp : type := pred predicate'} ❙
theory OneCuboid : base:?Logic =
......@@ -103,8 +113,14 @@ theory IntervalPartition : base:?Logic =
theory IntervalCartesianProduct : base:?Logic =
include ts:?TypedSets ❙
include ?Intervals ❙
include lfx:?LFSigma ❙
cIntervalToTuple : type_ci ⟶ (ℝ × ℝ) ❘ = [ci] ⟨ ci.left , ci.right ⟩❙
cIntervalToOrderedTyple : type_ci ⟶ (ℝ × ℝ) ❘ = [ci] ⟨ arith?RealArithmetics?min (ci.left) (ci.right) , arith?RealArithmetics?max (ci.left) (ci.right) ⟩ ❙
closedInvervalToSet : {a : ℝ} {b : ℝ} cInterval a b ⟶ set ℝ ❘ = [a , b , ci] ⟪ x : ℝ | min a b ≤ x ≤ max a b ⟫
closedInvervalToSet : type_ci ⟶ set ℝ ❘ = [ ci ] bsetst ℝ (fullset ℝ ) ([x : ℝ] arith?RealArithmetics?min (ci.left) (ci.right) ≤ x ∧ x ≤ arith?RealArithmetics?max (ci.left) (ci.right) )
\ 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