antitone_comp_ofDual_iff — Mathlib

English

For every pair of preordered sets α and β and every function f : α → β, f is monotone if and only if the composition f ∘ ofDual is antitone.

Русский

Пусть α и β являются множест-п предOrder; пусть f : α → β. Тогда f монотонна тогда и только тогда, когда композиция f ∘ ofDual антитонна.

LaTeX

$$$\operatorname{Antitone}(f \circ \mathrm{ofDual}) \iff \operatorname{Monotone}(f)$$$

Lean4

@[simp]
theorem antitone_comp_ofDual_iff : Antitone (f ∘ ofDual) ↔ Monotone f :=
  forall_swap

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