comap_map_le

Mathlib.MeasureTheory.MeasurableSpace.Basic

URI: https://scilib.ai/kg/mathlib#MeasurableSpace.comap_map_le

English

The comap of a mapped space is below the original space: (m.map f).comap f ≤ m.

Русский

Обратное отображение отображённой структуры по f не больше исходной структуры.

LaTeX

$$$$ (m.\mathrm{map}\, f).\mathrm{comap}\, f \le m $$$$

Lean4

theorem comap_map_le : (m.map f).comap f ≤ m :=
  (gc_comap_map f).l_u_le _

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

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

Разделы

Аффилиация

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