monovary_iff_exists_monotone — Mathlib

English

For f: ι → α, g: ι → β, Monovary f g holds if and only if there exists a linear order on ι such that both f and g are monotone on the whole domain.

Русский

Для f: ι → α, g: ι → β, Monovary f g выполняется тогда и только тогда, когда существует линейный порядок на ι, при котором f и g обе монотонны на всей области определения.

LaTeX

$$$\mathrm{Monovary}(f,g) \iff \exists\,(L: \text{LinearOrder } ι), \ \mathrm{Monotone}(f) \wedge \mathrm{Monotone}(g)$$$

Lean4

theorem monovary_iff_exists_monotone : Monovary f g ↔ ∃ (_ : LinearOrder ι), Monotone f ∧ Monotone g := by
  simp [← monovaryOn_univ, monovaryOn_iff_exists_monotoneOn]

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