strictMonoOn_comp_ofDual_iff — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

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

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