Commit da66d1f0 by Sven Wille

### partial functions

parent 04dee6ee
 ... ... @@ -4,6 +4,19 @@ namespace http://mathhub.info/MitM/smglom/calculus ❚ import base http://mathhub.info/MitM/Foundation ❚ import ts http://mathhub.info/MitM/smglom/typedsets ❚ import ms http://mathhub.info/MitM/smglom/measures ❚ import calc http://mathhub.info/MitM/smglom/calculus ❚ import exr http://mathhub.info/MitM/smglom/arithmetics ❚ theory IntervalPartition : base:?Logic = include ?Intervals ❙ partitionOfInterval : interval ⟶ type ❘ = [i] ❙ ❚ theory UpperLowerSum : base:?Logic = ❚ theory DarbouxIntegral : base:?Logic = ... ...
 ... ... @@ -100,4 +100,6 @@ theory Series : base:?Logic = axiom_partialSumStep : {G : metricMonoid} ⊦ ∀[S : G^ω] ∀[n] parSum S (succ_nat_lit n) ≐ (G.op) (parSum S n) (S (succ_nat_lit n)) ❙ prop_convergent : {G : metricMonoid} G^ω ⟶ prop ❘ = [G][S] prop_convergent G ([n] parSum S n) ❙ series : {G : metricMonoid, S: G^ω} dom G ❘ = [G,S] lim (partialSum G S) ❘ # SUM 2 ❙ ❚ \ No newline at end of file ❚
 namespace http://mathhub.info/MitM/smglom/typedsets ❚ import base http://mathhub.info/MitM/Foundation ❚ import fnd http://mathhub.info/MitM/Foundation ❚ import ts http://mathhub.info/MitM/smglom/typedsets ❚ // this file is mainly for documentation purposes on different ways on how to implement partial functions ❚ theory partialFunctions1 : base:?Logic = include fnd:?OptionType ❙ a : type ❙ bla : 𝒰 100 ❘ = Option a ❙ partialFunction : type ⟶ type ⟶ 𝒰 100 ❘= [a,b] a ⟶ Option b❙ ❚ theory partialFunctions2 : base:?Logic = include ts:?TypedSets ❙ partialFunction : type ⟶ type ⟶ type ❘ = [d,c] {' domain : set d , f : d ⟶ c'} ❘ # 1 →p 2❙ getDomain : {a : type} {b : type} partialFunction a b ⟶ set a❙ applyPartialFunction : {d : type} {c : type} d →p c ⟶ ❙ ❚ theory partialFunctions3 : base:?Logic = // use arbitary ❙ ❚ // u se sigme ❚ // use subset with proof ❚ \ 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!