Skip to content

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

Open
Brixfoly wants to merge 1 commit into
math-comp:masterfrom
Brixfoly:measurableTypeNormed
Open

Measurable type for normed modules (generalizes PR#2016)#2017
Brixfoly wants to merge 1 commit into
math-comp:masterfrom
Brixfoly:measurableTypeNormed

switch from sigma-algebra generated by ocitv to open sets

429e727
Select commit
Loading
Failed to load commit list.
Sign in for the full log view

Annotations

1 warning
rocq-core
succeeded Aug 12, 2026 in 1m 49s