English
Let f be an order-preserving bijection between ordered sets α and β. If f is concave on the entire domain, then the inverse function f^{-1} is convex on the entire domain.
Русский
Пусть f — биекция, сохраняющая порядок, между упорядоченными множествами α и β. Если f выпукла на всей области определения, то её обратная функция f^{-1} выпукла на всей области определения.
LaTeX
$$$$\\text{If } f:\\alpha \\to \\beta \\text{ is an order isomorphism and } f \\text{ is concave on } \\mathsf{univ}, \\text{ then } f^{-1}:\\beta \\to \\alpha \\text{ is convex on } \\mathsf{univ}.$$$$
Lean4
theorem convexOn_symm (f : α ≃o β) (hf : ConcaveOn 𝕜 univ f) : ConvexOn 𝕜 univ f.symm :=
by
refine ⟨convex_univ, fun x _ y _ a b ha hb hab => ?_⟩
obtain ⟨x', hx''⟩ := f.surjective.exists.mp ⟨x, rfl⟩
obtain ⟨y', hy''⟩ := f.surjective.exists.mp ⟨y, rfl⟩
simp only [hx'', hy'', OrderIso.symm_apply_apply]
rw [← f.le_iff_le, OrderIso.apply_symm_apply]
exact hf.2 (by simp : x' ∈ univ) (by simp : y' ∈ univ) ha hb hab
