monotoneOn_toDual_comp_iff — Mathlib

English

Let α, β be preorders and f : α → β. The restriction of toDual ∘ f to s is monotone iff the restriction of f to s is antitone.

Русский

Пусть α, β — предмножества. Тогда ограничение toDual ∘ f на $s$ монотонно тогда и только тогда, когда ограничение f на $s$ антитонно.

LaTeX

$$$\operatorname{MonotoneOn}(\mathrm{toDual} \circ f, s) \iff \operatorname{AntitoneOn}(f, s)$$$

Lean4

@[simp]
theorem monotoneOn_toDual_comp_iff : MonotoneOn (toDual ∘ f) s ↔ AntitoneOn f s :=
  Iff.rfl

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