Measurable type for normed modules (generalizes PR#2016)#2017

Open

Brixfoly wants to merge 3 commits into

math-comp:masterfrom

Brixfoly:measurableTypeNormed

Commits on Jul 3, 2026

switch from sigma-algebra generated by ocitv to open sets

committed

Commits on Jul 5, 2026

put most Import MeasurableR in sections
affeldt-aist
committed

Commits on Jul 7, 2026

generalized display from reals to normed modules
adjevahi
committed