monotone_prodMk_iff

Mathlib.Order.Monotone.Defs

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

← MathLib Explorer

English

The projection to the second coordinate is monotone.

Русский

Проекция на вторую координату монотонна.

LaTeX

$$$\text{Monotone}(\mathsf{Prod}.\mathsf{snd})$$$

Lean4

theorem monotone_prodMk_iff {f : γ → α} {g : γ → β} : Monotone (fun x => (f x, g x)) ↔ Monotone f ∧ Monotone g := by
  simp_rw [Monotone, Prod.mk_le_mk, forall_and]

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

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

Разделы

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

Аффилиация

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