Theorem null_frontier_inter

Modification history

2025-08-10 12:55

Mathlib/MeasureTheory/Constructions/BorelSpace/Basic.lean

feat: taking the product of probability measures is a continuous map (#27932)

Added null_frontier_inter View on Github →