monotone_fst

Mathlib.Order.Monotone.Defs

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

← MathLib Explorer

English

If f and g are monotone, then the pair map x ↦ (f x, g x) is monotone.

Русский

Если f и g монотонны, то отображение x ↦ (f x, g x) монотонно.

LaTeX

$$$(\forall x,y, x\le y \Rightarrow f(x)\le f(y)) \land (\forall x,y, x\le y \Rightarrow g(x)\le g(y)) \Rightarrow \forall x,y, x\le y \Rightarrow (f(x),g(x)) \le (f(y),g(y)).$$$

Lean4

theorem monotone_fst : Monotone (@Prod.fst α β) := fun _ _ ↦ And.left

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

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

Разделы

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

Аффилиация

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