monotoneOn_dual_iff — Mathlib

English

For any α, β with preorders and f, and subset s, MonotoneOn (toDual ∘ f ∘ ofDual) s is equivalent to MonotoneOn f s.

Русский

Для любых $\alpha, \beta$ с предориентированием и функции $f$, и подмножества $s$, монотонностьOn через двойственный порядок равносильна монотонности на исходном.

LaTeX

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

Lean4

theorem monotoneOn_dual_iff : MonotoneOn (toDual ∘ f ∘ ofDual : αᵒᵈ → βᵒᵈ) s ↔ MonotoneOn f s := by
  rw [monotoneOn_toDual_comp_iff, antitoneOn_comp_ofDual_iff]

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