Order and positivity of scalar multiples of measures

If a μ ≤ b μ for a nonzero measure μ and a positive scalar a, then b is positive.

Main results

• MeasureTheory.Measure.pos_of_smul_le_smul: if a μ ≤ b μ for a nonzero measure μ, with a > 0, then b > 0.

theorem MeasureTheory.Measure.pos_of_smul_le_smul {α : Type u_1} [MeasurableSpace α] {μ : Measure α} {a b : ENNReal} (ha : 0 < a) (h : a • μ ≤ b • μ) (hμ : μ ≠ 0) : 0 < b

If a μ ≤ b μ for a nonzero measure μ, with a > 0, then b > 0.