strictMonoOn_dual_iff — Mathlib

English

For any f and s, StrictMonoOn (toDual ∘ f ∘ ofDual) s ↔ StrictAntiOn f s.

Русский

Для любых $f$ и $s$ строгая монотонность на двойственном образе эквивалентна строгой антитонности на исходном.

LaTeX

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

Lean4

theorem strictMonoOn_dual_iff : StrictMonoOn (toDual ∘ f ∘ ofDual : αᵒᵈ → βᵒᵈ) s ↔ StrictMonoOn f s := by
  rw [strictMonoOn_toDual_comp_iff, strictAntiOn_comp_ofDual_iff]

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