namespace http://mathhub.info/MitM/core/calculus ❚
import base http://mathhub.info/MitM/Foundation ❚
import sets http://mathhub.info/MitM/core/typedsets ❚
import algebra http://mathhub.info/MitM/core/algebra ❚
import topo http://mathhub.info/MitM/core/topology ❚
theory MetricSpace : base:?Logic =
include arithmetics?RealArithmetics ❙
include ☞sets:?SetStructures ❙
theory signature_theory : base:?Logic =
include ☞sets:?SetStructures/setstruct_theory ❙
d : U ⟶ U ⟶ ℝ ❙
❚
signature = Mod ☞?MetricSpace/signature_theory ❙
prop_nonNegative : {G : type, d : G ⟶ G ⟶ ℝ} prop ❘ = [G,d] ∀[x]∀[y] 0 ≤ d x y ❙
prop_identityOfIndiscernibles : {G : type, d : G ⟶ G ⟶ ℝ} prop ❘ = [G,d] ∀[x]∀[y] d x y ≐ 0 ⇒ x ≐ y ❙
prop_positiveDefinite : {G : type, d : G ⟶ G ⟶ ℝ^+ }prop ❘ = [G,d] prop_nonNegative G d ∧ prop_identityOfIndiscernibles G d ❙
prop_symmetric : {G : type, d : G ⟶ G ⟶ ℝ} prop ❘
= [G][d] ∀[x]∀[y] d x y ≐ d y x ❙
prop_pseudoMetric : {G : type, d : G ⟶ G ⟶ ℝ^+} prop ❘ = [G,d] prop_positiveDefinite G d ∧ prop_symmetric G d ❙
theory pseudoMetricSpace_theory : base:?Logic =
include ☞sets:?SetStructures/setstruct_theory ❙
d : U ⟶ U ⟶ ℝ^+ ❙
axiom_isPseudoMetric : ⊦ prop_pseudoMetric U d ❙
❚
pseudoMetricSpace = Mod ☞?MetricSpace/pseudoMetricSpace_theory ❙
prop_triangleInequality : {G : type, d : G ⟶ G ⟶ ℝ} prop ❘
= [G][d] ∀[x]∀[y]∀[z] (d x z) ≤ ((d y x) + (d y z)) ❙
theory metricSpace_theory : base:?Logic =
include ?MetricSpace/pseudoMetricSpace_theory ❙
axiom_triangleInequality : ⊦ prop_triangleInequality U d ❙
❚
metricSpace = Mod ☞?MetricSpace/metricSpace_theory ❙
// metricSpace : type ⟶ type ❘ # metricSpace 1 ❙ // = [A] ⟨metricspace | ([G] ⊦ A ≐≐ G.universe)⟩❘
distanceFunction : type ⟶ type ❘ = ⟨A ⟶ A ⟶ ℝ | ([x] ⊦ ∃[G: metricSpace] x ≐ G.d)⟩ ❘ # distanceFunction 1 ❙
metric : {G: metricSpace} (G.universe ⟶ G.universe ⟶ ℝ) ❘ # d 2 3 ❘ = [G][a][b] (G.d) a b ❙
❚
theory MetricMonoid : base:?Logic =
include ?MetricSpace ❙
include algebra?Monoid❙
theory metricMonoid_theory : base:?Logic =
include algebra?Monoid/monoid_theory ❙
include ?MetricSpace/metricSpace_theory ❙
❚
metricMonoid = Mod ☞?MetricMonoid/metricMonoid_theory ❙
❚
theory Ball : base:?Logic =
include ?MetricSpace ❙
include ☞sets:?AllSets ❙
openBall : {M: metricSpace} M.universe ⟶ ℝ ⟶ set (M.universe) ❘
= [M][a][ε] ⟪ (doms M) | ([x] (d x a) < ε) ⟫ ❘ # B_ 3 2❙
closedBall : {M: metricSpace} M.universe ⟶ ℝ ⟶ set (M.universe) ❘
= [M][a][ε] ⟪ (doms M) | ([x] (d x a) ≤ ε) ⟫ ❙ // MiKo: how to do \overline{B} in the notation? ❙
❚
theory MetricSpaceAsTopology : base:?Logic =
include ?Ball ❙
include ☞topo:?HausdorffTopology ❙
// Why only Hausdorff? Don't we obtain even stronger conditions (normal?)? ❙
// A: as soon as we formalized those, sure :) ❙
openColl : {M : metricSpace} set (set (dom M)) ❙
axiom_ballIsOpen : {M : metricSpace, a : M.universe, ε : ℝ} ⊦ (openBall M a ε) ∈ (openColl M) ❙
axiom_emptyIsOpen : {M : metricSpace} ⊦ prop_emptyInColl (openColl M) ❘ # emptyisopen 1 ❙
axiom_fullIsOpen : {M : metricSpace} ⊦ prop_fullInColl (openColl M) ❘ # fullisopen 1 ❙
axiom_unionIsOpen : {M : metricSpace} ⊦ prop_unionInColl (openColl M) ❘ # unionisopen 1 ❙
axiom_intersectionIsOpen : {M : metricSpace} ⊦ prop_finiteIntersection (openColl M) ❘ # intersectionisopen 1 ❙
axiom_metricIsHausdorff : {M : metricSpace} ⊦ hausdorffProperty (dom M) (openColl M) ❘ # miHaus 1 ❙
metricAsTopology : {M : metricSpace}hausdorffTopology (dom M) ❘
= [M] ['
universe := M.universe,
d := M.d,
axiom_isPseudoMetric := M.axiom_isPseudoMetric,
axiom_triangleInequality := M.axiom_triangleInequality,
coll := openColl M,
axiom_empty := axiom_emptyIsOpen M,
axiom_full := axiom_fullIsOpen M,
☞?OML?axiom_union := axiom_unionIsOpen M,
axiom_intersection := axiom_intersectionIsOpen M,
ishausdorff := miHaus M
'] ❙
❚
theory RealMetricSpace : base:?Logic =
include arithmetics?RealArithmetics ❙
include ?MetricSpace ❙
realmetric : ℝ ⟶ ℝ ⟶ ℝ^+ ❘ = [a,b] | a - b | ❘ # ds 1 , 2 ❙
axiom_realIsPseudoMetric : ⊦ prop_pseudoMetric ℝ realmetric ❙
axiom_triangleReal : ⊦ prop_triangleInequality ℝ realmetric ❙
realmetricspace : metricSpace ❘
= ['
universe := ℝ,
d := realmetric,
axiom_isPseudoMetric := axiom_realIsPseudoMetric,
axiom_triangleInequality := axiom_triangleReal
'] ❘ # ℝm ❙
axiom_predRealIsPseudoMetric : {P : ℝ ⟶ bool} ⊦ prop_pseudoMetric (pred P) realmetric ❘ # pseudom 1 ❙
axiom_predTriangle : {P : ℝ ⟶ bool} ⊦ prop_triangleInequality (pred P) realmetric ❘ # realmet 1 ❙
realSubMetric : {P : ℝ ⟶ bool} metricSpace ❘
= [P] ['
universe := pred P,
d := [a : pred P][b : pred P] realmetric a b,
axiom_isPseudoMetric := pseudom P,
axiom_triangleInequality := realmet P
'] ❘ # mpred 1 ❙
axiom_mpredIsSuptype : {P : ℝ ⟶ bool} (mpred P).universe <* ℝ ❙
❚