monovaryOn_iff_exists_antitoneOn — Mathlib

English

For f: ι → α, g: ι → β and s ⊆ ι, MonovaryOn f g s holds if and only if there exists a linear order on ι under which f is monotone on s and g is antitone on s.

Русский

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

LaTeX

$$$\mathrm{MonovaryOn}(f,g,s) \iff \exists\,(L: \text{LinearOrder } ι), \ \mathrm{MonotoneOn}(f,s) \wedge \mathrm{AntitoneOn}(g,s)$$$

Lean4

theorem monovaryOn_iff_exists_antitoneOn : MonovaryOn f g s ↔ ∃ (_ : LinearOrder ι), AntitoneOn f s ∧ AntitoneOn g s :=
  by simp_rw [← antivaryOn_toDual_left, antivaryOn_iff_exists_monotoneOn_antitoneOn, monotoneOn_toDual_comp_iff]

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