prodMap — Mathlib

English

If f and g are strictly monotone, then Prod.map f g is strictly monotone.

Русский

Если f и g строго монотонны, то Prod.map f g строго монотонна.

LaTeX

$$$\text{StrictMono } f \to \text{StrictMono } g \to \text{StrictMono } (\text{Prod}.\text{map } f g)$$$

Lean4

theorem prodMap (hf : StrictMono f) (hg : StrictMono g) : StrictMono (Prod.map f g) := fun a b ↦
  by
  simp only [Prod.lt_iff]
  exact Or.imp (And.imp hf.imp hg.monotone.imp) (And.imp hf.monotone.imp hg.imp)

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