strictAntiOn_dual_iff — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

theorem strictAntiOn_dual_iff : StrictAntiOn (toDual ∘ f ∘ ofDual : αᵒᵈ → βᵒᵈ) s ↔ StrictAntiOn f s := by
  rw [strictAntiOn_toDual_comp_iff, strictMonoOn_comp_ofDual_iff]

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