join_zero

Mathlib.MeasureTheory.Measure.GiryMonad

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

English

The join of the zero measure is zero: (0 : Measure (Measure α)).join = 0.

Русский

Склейка нулевой меры равна нулю: (0 : Measure (Measure α)).join = 0.

LaTeX

$$$\\text{join }0 = 0$$$

Lean4

@[simp]
theorem join_zero : (0 : Measure (Measure α)).join = 0 :=
  by
  ext1 s hs
  simp [hs]

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

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

Разделы

Аффилиация

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