isZeroOrProbabilityMeasureSMul — Mathlib

English

For any μ, ((μ univ)⁻¹ • μ) is a zero-or-probability measure.

Русский

Для любой μ нормализованная мера ((μ univ)⁻¹ • μ) является нулевой или вероятностной.

LaTeX

$$$\mathrm{IsZeroOrProbabilityMeasure}(((\mu\ univ)^{-1}) \cdot \mu)$$$

Lean4

instance isZeroOrProbabilityMeasureSMul : IsZeroOrProbabilityMeasure ((μ univ)⁻¹ • μ) :=
  by
  rcases eq_zero_or_neZero μ with rfl | h
  · simp; infer_instance
  rcases eq_top_or_lt_top (μ univ) with h | h
  · simp [h]; infer_instance
  have : IsFiniteMeasure μ := ⟨h⟩
  infer_instance

Похожие утверждения