Monotone on product order

Stream: Is there code for X?

[Aaron Liu]

I couldn't find these in mathlib

import Mathlib

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

theorem Monotone.prodMk {α β γ : Type*} [Preorder α] [Preorder β] [Preorder γ]
    {f : γ → α} {g : γ → β} (hf : Monotone f) (hg : Monotone g) : Monotone (fun x => (f x, g x)) :=
  monotone_prodMk_iff.2 ⟨hf, hg⟩

[Aaron Liu]

p.s. should Monotone be a fun_prop goal?

[Ruben Van de Velde]

Please pr :)

[Aaron Liu]

#28050