sub_zero

Mathlib.MeasureTheory.Measure.Sub

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

English

μ - 0 = μ.

Русский

μ - 0 = μ.

LaTeX

$$$\\\\mu - 0 = \\\\mu$$$

Lean4

@[simp]
protected theorem sub_zero : μ - 0 = μ := by
  rw [sub_def]
  apply le_antisymm
  · simp [sInf_le]
  · simp

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

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

Разделы

Аффилиация

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