measureReal_empty — Mathlib

English

The real-valued characteristic of the zero-measure part satisfies basic algebraic identities; in particular, the real part of the zero measure is zero.

Русский

Реальная часть нулевой меры удовлетворяет базовым тождествам; в частности, реальная часть нулевой меры равна нулю.

LaTeX

$$μ.real ∅ = 0$$

Lean4

@[simp]
theorem measureReal_empty : μ.real ∅ = 0 := by simp [Measure.real]

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