smul_filter_le_smul_filter

Mathlib.Order.Filter.Pointwise

URI: https://scilib.ai/kg/mathlib#Filter.smul_filter_le_smul_filter

English

If f1 ≤ f2 then a • f1 ≤ a • f2.

Русский

Если f1 ≤ f2, то a • f1 ≤ a • f2.

LaTeX

$$$ (f_1 \le f_2) \Rightarrow (a \cdot f_1 \le a \cdot f_2) $$$

Lean4

@[to_additive]
theorem smul_filter_le_smul_filter (hf : f₁ ≤ f₂) : a • f₁ ≤ a • f₂ :=
  map_mono hf

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

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

Разделы

Аффилиация

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