map_mono

Mathlib.MeasureTheory.OuterMeasure.Operations

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

English

For any f, map f is monotone: if m ≤ n then map f m ≤ map f n.

Русский

Для любой f мапа монотонна: если m ≤ n, то map f m ≤ map f n.

LaTeX

$$$ m \le n \Rightarrow map\ f\ m \le map\ f\ n $$$

Lean4

@[mono]
theorem map_mono {β} (f : α → β) : Monotone (map f) := fun _ _ h _ => h _

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

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

Разделы

Аффилиация

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