trim_eq_self

Mathlib.MeasureTheory.Measure.Trim

URI: https://scilib.ai/kg/mathlib#MeasureTheory.trim_eq_self

English

For any measure μ, μ.trim = μ when trimmed along le_rfl.

Русский

Для любой меры μ обрезка μ по отношению к μ равна μ.

LaTeX

$$$\\mu^{\\text{trim}} = \\mu$$$

Lean4

@[simp]
theorem trim_eq_self [MeasurableSpace α] {μ : Measure α} : μ.trim le_rfl = μ := by simp [Measure.trim]

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

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

Разделы

Аффилиация

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