antitone_toDual_comp_iff — Mathlib

English

For every pair of preordered sets α and β and every f : α → β, the antitone property of f is equivalent to the monotonicity of toDual ∘ f.

Русский

Пусть α и β — множества с предор; f : α → β. Тогда антитонность f эквивалентна монотонности toDual ∘ f.

LaTeX

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

Lean4

@[simp]
theorem antitone_toDual_comp_iff : Antitone (toDual ∘ f) ↔ Monotone f :=
  Iff.rfl

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