map_comap_le

Mathlib.MeasureTheory.OuterMeasure.Operations

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

English

For any f and OuterMeasure m, we have map f (comap f m) ≤ m.

Русский

Для любой функции f и внешней меры m выполняется неравенство: map f (comap f m) ≤ m.

LaTeX

$$$ map\ f\ (comap\ f\ m) \le m $$$

Lean4

theorem map_comap_le {β} (f : α → β) (m : OuterMeasure β) : map f (comap f m) ≤ m := fun _ =>
  m.mono <| image_preimage_subset _ _

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

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

Разделы

Аффилиация

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