map_mono

Mathlib.MeasureTheory.MeasurableSpace.Basic

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

English

If m1 ≤ m2 then m1.map f ≤ m2.map f.

Русский

Если m1≤m2, то m1.map f ≤ m2.map f.

LaTeX

$$$m_1 \le m_2 \Rightarrow m_1.map f \le m_2.map f$$$

Lean4

theorem map_mono (h : m₁ ≤ m₂) : m₁.map f ≤ m₂.map f :=
  (gc_comap_map f).monotone_u h

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

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

Разделы

Аффилиация

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