This doesnβt look right to me, as surely the topology is derived from the metric, rather than metric space material being adjoined to a topology.
In HOL Light, a metric space is an abstract type represented by pairs (S,d) where S is the carrier and d is the distance function. Could that be the best approach for us, or should we use a locale? But then the notion of a metric space is a property rather than a type. Larry > On 16 Apr 2019, at 14:08, Fabian Immler <[email protected]> wrote: > > Combining it with the anonymous relativization efforts > https://github.com/xanonec/HOL-Types_To_Sets_Ext/blob/master/Topology/Topological_Space_OW.thy#L52 > it could look like this: > > locale topological_space_ow = > fixes π :: "'at set" and Ο :: "'at set β bool" > assumes open_UNIV[simp, intro]: "Ο π" > assumes open_Int[intro]: "β¦ S β π; T β π; Ο S; Ο T β§ βΉ Ο (S β© T)" > assumes open_Union[intro]: "β¦ K β Pow π; βSβK. Ο S β§ βΉ Ο (βK)" > > locale metric_space_ow = topological_space_ow + > fixes dist:: "'at β 'at β real" > assumes open_dist: "S β π βΉ Ο S β· (βxβS. βe>0. βy. dist y x < e βΆ y β S)" > assumes dist_eq_0_iff [simp]: "x β π βΉ y β π βΉ dist x y = 0 β· x = y" > and dist_triangle2: "x β π βΉ y β π βΉ dist x y β€ dist x z + dist y z" > > > Of course, this is yet another approach and different from the > "topology-as-value" approach from Abstract_Topology > (http://isabelle.in.tum.de/repos/isabelle/file/538919322852/src/HOL/Analysis/Abstract_Topology.thy#l19) > > One would need to think about if or how it makes sense to combine such a > "locale-only" approach with a "topology-as-value"/"metric-space-as-value" > approach. (Projecting the topology out of the metric-space value and having > these as parameters of the locales?) > > Fabian _______________________________________________ isabelle-dev mailing list [email protected] https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev
