monovary_iff_exists_antitone — Mathlib

English

For f: ι → α, g: ι → β, Monovary f g holds if and only if there exists a linear order on ι under which f and g are both antitone on the domain.

Русский

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

LaTeX

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

Lean4

theorem monovary_iff_exists_antitone : Monovary f g ↔ ∃ (_ : LinearOrder ι), Antitone f ∧ Antitone g := by
  simp [← monovaryOn_univ, monovaryOn_iff_exists_antitoneOn]

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