div_le_div

Mathlib.Order.Filter.Pointwise

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

English

Division is monotone in both arguments: if f1 ≤ f2 and g1 ≤ g2 then f1 / g1 ≤ f2 / g2.

Русский

Деление монотонно по обоим аргументам: если f1 ≤ f2 и g1 ≤ g2, то f1 / g1 ≤ f2 / g2.

LaTeX

$$$f_1 \\le f_2 \\land g_1 \\le g_2 \\Rightarrow f_1 / g_1 \\le f_2 / g_2.$$$

Lean4

@[to_additive]
protected theorem div_le_div : f₁ ≤ f₂ → g₁ ≤ g₂ → f₁ / g₁ ≤ f₂ / g₂ :=
  map₂_mono

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

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

Разделы

Аффилиация

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