le_comap_map

Mathlib.MeasureTheory.OuterMeasure.Operations

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

English

For any f and OuterMeasure m on α, we have

Русский

Для любой функции f и внешней меры m на α выполняется неравенство:

LaTeX

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

Lean4

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

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

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

Разделы

Аффилиация

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