monotoneOn_comp_ofDual_iff — Mathlib

English

Let α be a preorder and s ⊆ α. Then the restriction of f ∘ ofDual to s is monotone iff the restriction of f to s is antitone.

Русский

Пусть α — предпорядок и $s ⊆ α$. Тогда ограничение $f \circ \mathrm{ofDual}$ на $s$ монотонно тогда и только тогда, когда ограничение $f$ на $s$ антитонно.

LaTeX

$$$\operatorname{MonotoneOn}(f \circ \mathrm{ofDual}, s) \iff \operatorname{AntitoneOn}(f, s)$$$

Lean4

@[simp]
theorem monotoneOn_comp_ofDual_iff : MonotoneOn (f ∘ ofDual) s ↔ AntitoneOn f s :=
  forall₂_swap

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