inv — Mathlib

English

If f: β → α is monotone, then the map x ↦ f(x)^{-1} is antitone (order-reversing).

Русский

Если f: β → α монотонна, то отображение x ↦ f(x)^{-1} является антитонной (обращение порядка).

LaTeX

$$$ \text{Monotone}(f) \Rightarrow \text{Antitone}(x \mapsto f(x)^{-1}). $$$

Lean4

@[to_additive]
theorem inv (hf : Monotone f) : Antitone fun x => (f x)⁻¹ := fun _ _ hxy => inv_le_inv_iff.2 (hf hxy)

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