strictAntiOn_toDual_comp_iff — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

@[simp]
theorem strictAntiOn_toDual_comp_iff : StrictAntiOn (toDual ∘ f : α → βᵒᵈ) s ↔ StrictMonoOn f s :=
  Iff.rfl

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