instSFiniteFstOfProd

Mathlib.MeasureTheory.Measure.Prod

URI: https://scilib.ai/kg/mathlib#MeasureTheory.Measure.instSFiniteFstOfProd

English

If a measure ρ on α × β is s-finite, then its first marginal ρ.fst is s-finite as well.

Русский

Если ρ на α×β является s-финитной, то его первая маргинальная мера ρ.fst тоже s-финитная.

LaTeX

$$$$\\text{If } \\rho \\text{ is } SFinite,\\; \\rho.fst \\text{ is also } SFinite.$$$$

Lean4

instance [SFinite ρ] : SFinite ρ.fst := by
  rw [fst]
  infer_instance

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

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

Разделы

Аффилиация

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