antitoneOn_iff_antitone — Mathlib

English

Let f: α → β and s ⊆ α. Then f is antitone on s if and only if the restricted map a ↦ f(a) on s is antitone: AntitoneOn f s ⇔ Antitone (λ a : s. f(a)).

Русский

Пусть f: α → β и s ⊆ α. Тогда f антимонотонна на s тогда и только тогда ограниченная функция a ↦ f(a) на s антимонотонна: AntitoneOn f s ⇔ Antitone (λ a : s. f(a)).

LaTeX

$$$ \operatorname{AntitoneOn}(f,s) \iff \operatorname{Antitone}(\lambda a : s. f(a))$$$

Lean4

theorem antitoneOn_iff_antitone : AntitoneOn f s ↔ Antitone fun a : s => f a := by simp [Antitone, AntitoneOn]

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