le_map_add_map_div'

Mathlib.Algebra.Order.Hom.Basic

URI: https://scilib.ai/kg/mathlib#le_map_add_map_div'

← MathLib Explorer

English

For suitable f and x,y, we have f(x) ≤ f(y) + f(y/x).

Русский

Для подходящего f и x,y выполняется f(x) ≤ f(y) + f(y/x).

LaTeX

$$$f(x) \le f(y) + f\left(\frac{y}{x}\right)$$$

Lean4

@[to_additive]
theorem le_map_add_map_div' : f x ≤ f y + f (y / x) := by
  simpa only [add_comm, map_div_rev, div_mul_cancel] using map_mul_le_add f (x / y) y

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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