strictAntiOn_comp_ofDual_iff — Mathlib

English

For any f and subset s, StrictAntiOn (f ∘ ofDual) s is equivalent to StrictMonoOn f s.

Русский

Для любой $f$ и подмножества $s$ строгая антитонность на $s$ композиции $f \circ \mathrm{ofDual}$ эквивалентна строгой монотонности на $s$ функции $f$.

LaTeX

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

Lean4

@[simp]
theorem strictAntiOn_comp_ofDual_iff : StrictAntiOn (f ∘ ofDual) s ↔ StrictMonoOn f s :=
  forall₂_swap

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