isFiniteMeasure_iff — Mathlib

English

If X has a law with respect to μ and P, then μ is a probability measure iff P is a probability measure.

Русский

Если X имеет закон по отношению к μ и P, то μ является вероятностной мерой тогда и только тогда, когда P является вероятностной мерой.

LaTeX

$$$$ \\text{HasLaw } X\\; \\mu\\; P \\Rightarrow (\\operatorname{IsProbabilityMeasure} \\mu \\leftrightarrow \\operatorname{IsProbabilityMeasure} P) $$$$

Lean4

protected theorem isFiniteMeasure_iff (hX : HasLaw X μ P) : IsFiniteMeasure μ ↔ IsFiniteMeasure P := by
  rw [← hX.map_eq, isFiniteMeasure_map_iff hX.aemeasurable]

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