instSFiniteSndOfProd

Mathlib.MeasureTheory.Measure.Prod

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

English

If ρ is s-finite, then ρ.snd is s-finite, as an instance.

Русский

Если ρ сивфинитна, то ρ.snd тоже сивфинитна, как экземпляр.

LaTeX

$$$$ \\text{If } SFinite(\\rho) \\text{ then } SFinite(\\rho.snd). $$$$

Lean4

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

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

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

Разделы

Аффилиация

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