id

Mathlib.Probability.HasLaw

URI: https://scilib.ai/kg/mathlib#ProbabilityTheory.HasLaw.id

English

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

Русский

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

LaTeX

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

Lean4

protected theorem id : HasLaw id μ μ where map_eq := map_id

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru