Theorem MeasureTheory.VectorMeasure.tendsto_vectorMeasure_iInter_atTop_nat

Modification history

2026-01-26 09:20
Mathlib/MeasureTheory/VectorMeasure/Basic.lean
feat: more basic API on vector measures (#34414) …
Added MeasureTheory.VectorMeasure.tendsto_vectorMeasure_iInter_atTop_natView on Github →