`PhysMeasureBasis.cond_diffuse_noAtoms` {α : Type*} [MeasurableSpace α] [MeasurableSingletonClass α] (μ : Measure α) [IsFiniteMeasure μ] (_hpos : μ {x

Initializing...

`PhysMeasureBasis.cond_diffuse_noAtoms` {α : Type*} [MeasurableSpace α] [MeasurableSingletonClass α] (μ : Measure α) [IsFiniteMeasure μ] (_hpos : μ {x | μ {x} ≠ 0}ᶜ ≠ 0) : NullSing · Prove2Me