antitoneOn_toDual_comp_iff — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

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

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