strictMonoOn_mul_self

Mathlib.Algebra.Order.GroupWithZero.Unbundled.Basic

URI: https://scilib.ai/kg/mathlib#strictMonoOn_mul_self

← MathLib Explorer

English

The function x ↦ x^2 is strictly increasing on the set {x ≥ 0}.

Русский

Функция x ↦ x^2 строго возрастает на множестве {x ≥ 0}.

LaTeX

$$$ \\text{StrictMonoOn}(\\lambda x. x^2, \\{x \\ge 0\\}) $$$

Lean4

theorem strictMonoOn_mul_self [PosMulStrictMono M₀] [MulPosMono M₀] : StrictMonoOn (fun x ↦ x * x) {x : M₀ | 0 ≤ x} :=
  fun _ hx _ _ hxy ↦ mul_self_lt_mul_self hx hxy

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

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

Разделы

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

Аффилиация

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