[Brixfoly]

Motivation for this change

The main goal of this PR is to introduce the module MeasurableNormedModuleOpen
that equips a normed module N with a sigma-algebra (of open sets).
We want to do that to generalize the type of simple functions in simple_functions.v
to return in a normed module (instead of a realType).

The sigma-algebra for normed modules is kept in a module and therefore
available through an Import command. (This is maybe not necessary and we will
maybe remove this limitation later once this PR has been tested against @Brixfoly's work.)

This PR also fixes the sigma-algebra of ¥bar R so that it builds from the sigma-algebra
of open sets of R instead of octiv (but this is an orthogonal issue with no impact on end-users).

This PR also removes several global hint that were barely used for clarity and renames
a couple of lemmas that had the same identifiers.

fyi @affeldt-aist @hoheinzollern

This PR is used in #2170 to developed bochner.v (not reviewed yet, just rebased).

Checklist

• added corresponding entries in CHANGELOG_UNRELEASED.md

• added corresponding documentation in the headers

Reference: How to document

Merge policy

As a rule of thumb:

• PRs with several commits that make sense individually and that
  all compile are preferentially merged into master.
• PRs with disorganized commits are very likely to be squash-rebased.

Reminder to reviewers

• Read this Checklist
• Put a milestone if possible
• Check labels

[affeldt-aist]

@CohenCyril we need your input for this PR some time this week if possible

[Brixfoly]

I've implemented your recommendations and rebase the whole thing, now we can focus on the HB issues I think

[t6s]

I want to see a more detailed motivation comment before reviewing the code changes.

[affeldt-aist]

I want to see a more detailed motivation comment before reviewing the code changes.

I have edited the first item of the conversation for that.