Commit 9b58c127 authored by Sven Wille's avatar Sven Wille

more stuff

parent 6df94c50
namespace http://mathhub.info/MitM/smglom/algebra ❚
import top http://mathhub.info/MitM/interfaces❚
import base http://mathhub.info/MitM/Foundation ❚
import num http://mathhub.info/MitM/smglom/arithmetics ❚
import sets http://mathhub.info/MitM/smglom/typedsets ❚
import arith http://mathhub.info/MitM/smglom/arithmetics ❚
theory vectorFunctions : base:?Logic =
include base:?Vectors ❙
include arith:?NaturalArithmetics❙
vector_at : {A : type} {n : ℕ} {m : ℕ } vector A n ⟶ ⊦ m < n ⟶ A ❘# vector_at 3 4 5❙
vector_add : {n : ℕ} vector ℝ n ⟶ vector ℝ n ⟶ vector ℝ n❙
theory realcoordinatespace : base:Logic =
prop_implements_vectorspace ❙
\ No newline at end of file
......@@ -96,8 +96,15 @@ theory GeneralDomains : base:?Logic =
theory IntervalPartition : base:?Logic =
include ?Intervals ❙
include top:?FinSeqProps ❙
// include top:?FinSeqProps ❙
// intervalPartition : interval ⟶ type ❘ = [i] ❙
prop_is_closedinterval_partittion : {l : ℝ } {r : ℝ} {n : INat} cInterval l r ⟶ finSeq n ℝ ⟶ prop ❘ = [l,r,n, ci, fs] strictly_ascending fs ❙
// prop_is_closedinterval_partittion : {l : ℝ } {r : ℝ} {n : INat} cInterval l r ⟶ finSeq n ℝ ⟶ prop ❘ = [l,r,n, ci, fs] strictly_ascending fs ❙
theory IntervalCartesianProduct : base:?Logic =
include ?Intervals ❙
closedInvervalToSet : {a : ℝ} {b : ℝ} cInterval a b ⟶ set ℝ ❘ = [a , b , ci] ⟪ x : ℝ | min a b ≤ x ≤ max a b ⟫❙
\ No newline at end of file
......@@ -3,6 +3,7 @@ namespace http://mathhub.info/MitM/smglom/measures ❚
import base http://mathhub.info/MitM/Foundation ❚
import ts http://mathhub.info/MitM/smglom/typedsets ❚
import alg http://mathhub.info/MitM/smglom/algebra ❚
import arith http://mathhub.info/MitM/smglom/arithmetics ❚
theory SigmaOperator : base:?Logic =
......@@ -27,8 +28,11 @@ theory SigmaOperatorTheorems : base:?Logic =
theory BorelExample : base:?Logic =
include alg:?Productspace ❙
n : nat ❙
Ω = ❙
include base:?Vectors ❙
include arith:?NaturalNumbers ❙
n : ℕ ❙
// vspace = finite_vectorspace realfield n ❙ // this line crashes intellij ❙
Ω = vector ℝ n❙
ndimQuardRat = ⟨ vector ℝ n | ⟩ ❙
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