Commit 96d56c05 authored by Dennis Müller's avatar Dennis Müller

update

parent b97b5d83
......@@ -26,7 +26,7 @@ theory GroupAction : base:?Logic =
groupAction = Mod groupAction_theory❙
outer_notation : {GX : groupAction, g : dom GX, x : GX.X} GX.X ❘= [GX,g,x] ((GX.phi) g) x ❘# 2 < 3 > ❙
orbit : type ❙
polynomialOrbit : type ❙
theory PermutationGroup : base:?Logic =
......
......@@ -72,11 +72,11 @@ theory GeneralDomains : base:?Logic =
include ?MetricSpace/metricSpace_theory ❙
dimension : ℕ ❙
domainPred : U ⟶ prop ❙
domain : type ❘ = ⟨ U | ([x] ⊦ domainPred x) ⟩ ❙
domain : type ❘ = ⟨ x : U | ⊦ domainPred x ⟩ ❙
boundaryPred1 : U ⟶ prop ❘ = [b] ∀ [ε : ℝ+] ∃[x : domain] d x b < ε ❙
boundaryPred2 : U ⟶ prop ❘ = [b] ∀ [ε : ℝ+] ∃[x : U] d x b < ε ∧ ¬ domainPred x ❙
boundaryPred : U ⟶ prop ❘ = [b] boundaryPred1 b ∧ boundaryPred2 b ❙
boundary : type ❘ = ⟨ U | ([x] ⊦ boundaryPred x) ⟩ ❙
boundary : type ❘ = ⟨ x : U | ⊦ boundaryPred x ⟩ ❙
generalDomain = Mod `?GeneralDomains/generalDomain_theory ❙
......
......@@ -14,7 +14,7 @@ theory NormedSpace : base:?Logic =
include algebra:?Vectorspace/vectorspace_theory (realField) ❙
norm : universe ⟶ ℝ^+ ❘ # || 1 || ❙
axiom_multiplicativity : ⊦ ∀[x : universe] ∀[α : ℝ] `arith:?RealArithmetics?multiplication | α | || x || ≐ || (scalarmult) α x ||❘ // ⊦ || α ⋅ x || ≐ | α | ⋅ || x ||
axiom_multiplicativity : ⊦ ∀[x : universe] ∀[a : ℝ] `arith:?RealArithmetics?multiplication (`arith?RealArithmetics?absolute a) || x || ≐ || (scalarmult) a x ||
axiom_subadditivity : ⊦ ∀[x : universe] ∀[y : universe] (|| op x y ||) ≤ (||x|| + ||y||) ❘// ⊦ ||(x + y)|| ≤ (||x|| + ||y||) ❙
axiom_positivity : ⊦ ∀[x : universe] 0 ≤ || x || ❙
axiom_definiteness : ⊦ ∀[x : universe] 0.0 ≐ || x || ⇔ x ≐ unit ❙ // ⊦ ||x||≐0 ⇔ x ≐ e ❙
......
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