map_id

Mathlib.MeasureTheory.OuterMeasure.Operations

URI: https://scilib.ai/kg/mathlib#MeasureTheory.OuterMeasure.map_id

English

For every outer measure m, map id m = m.

Русский

Для любой внешней меры m выполняется map id m = m.

LaTeX

$$$ map(\mathrm{id}, m) = m $$$

Lean4

@[simp]
theorem map_id (m : OuterMeasure α) : map id m = m :=
  ext fun _ => rfl

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

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

Разделы

Аффилиация

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