monotone_comp_ofDual_iff — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

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

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