monotone_map

Mathlib.MeasureTheory.MeasurableSpace.Basic

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

English

The map operation is monotone in its argument.

Русский

Операция map монотонна по аргументу.

LaTeX

$$$\operatorname{Monotone}(\mathrm{MeasurableSpace.map} f)$$$

Lean4

theorem monotone_map : Monotone (MeasurableSpace.map f) := fun _ _ => map_mono

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

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

Разделы

Аффилиация

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