[_0w8t]

I got impression that intuitionistic mathematical analysis refers to original Boyer papers. Which is in modern terminology is constructive mathematical analysis plus an axiom of the choice sequence. Intuitionistic logic on the other hand is a classical logic without the law of excluded middle. This is what the constructive mathematics uses and which was also used by Boyer.

And yes, as in practice all physically measurable spaces are of finite dimensions, so using a formalism that works assuming AoC for arbitrary spaces is OK. The only danger is that one reads too much from it and assumes that the real world is like that.