ax5 added to PseudoMetric.mixin_of

[affeldt-aist]

• does not compile
• and there is an admit

[mkerjean]

I am not sure to understand why fct_open_ball should be true. Isn't there some continuity hypothesis at stake ?

[CohenCyril]

Actually, I don't even think continuity is enough. There is no reason for this to be true.
It seems we have to backtrack on our decision to add ax5 and introduce open_ball x e = (ball x e)° instead... WDYT?

[affeldt-aist]

by adding a topological structure to zmodType, I am afraid I start doing things that look like PR #205

[CohenCyril]

by adding a topological structure to zmodType, I am afraid I start doing things that look like PR #205

One should not do that, you are adding a trivial topology where everything is open, indeed you defined singletons to be open, hence any set, as an arbitrary union of singletons is automatically open...

Moreover, if you were to add the discrete topology instead, it would be incompatible with any other topology that we use... If one really need discrete topologies, they need to introduce an alias discrete T := T and have canonicals on discrete instead...

[affeldt-aist]

well, this was really to keep going and uncover more problems, if we are to have a topologicalType as a parameter of the pseudometric mixin then the end of the file needs to be changed for we cannot used topologyOfEntourageMixin anymore, am I wrong?

[CohenCyril]

well, this was really to keep going and uncover more problems, if we are to have a topologicalType as a parameter of the pseudometric mixin then the end of the file needs to be changed for we cannot used topologyOfEntourageMixin anymore, am I wrong?

I'm not sure I understand...

[affeldt-aist]

well, this was really to keep going and uncover more problems, if we are to have a topologicalType as a parameter of the pseudometric mixin then the end of the file needs to be changed for we cannot used topologyOfEntourageMixin anymore, am I wrong?

I'm not sure I understand...

I think that normedZ zmodType needs to be given its topological structure earlier

[CohenCyril]

I think that normedZ zmodType needs to be given its topological structure earlier

I do not understand why you say that, moreover zmodType should not have a canonical structure...

[affeldt-aist]

I think that normedZ zmodType needs to be given its topological structure earlier

I do not understand why you say that, moreover zmodType should not have a canonical structure...

It was to type check the open (ball_ Num.Def.normr x e) statement at line 4364 (though now we know that we can't do with this axiom anyway).

[CohenCyril]

It was to type check the open (ball_ Num.Def.normr x e) statement at line 4364 (though now we know that we can't do with this axiom anyway).

Then all you need is the topology of a normedZmodType structure, and it must and should not be canonical, but local, since we are defining a factory on this line.

[affeldt-aist]

It was to type check the open (ball_ Num.Def.normr x e) statement at line 4364 (though now we know that we can't do with this axiom anyway).

Then all you need is the topology of a normedZmodType structure, and it must and should not be canonical, but local, since we are defining a factory on this line.

I'll go back to it asap once ax5 is fixed as you suggested above.

[affeldt-aist]

We gave up extending the interface of pseudometric spaces. This PR is scheduled to be closed as it is. A related discussion is going on in PR #283 .