English
Let f be an order-preserving bijection between ordered sets α and β. If f is strictly concave on the entire domain, then the inverse function f^{-1} is strictly 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 strictly concave on } \\mathsf{univ}, \\text{ then } f^{-1}:\\beta \\to \\alpha \\text{ is strictly convex on } \\mathsf{univ}.$$$$
Lean4
theorem strictConvexOn_symm (f : α ≃o β) (hf : StrictConcaveOn 𝕜 univ f) : StrictConvexOn 𝕜 univ f.symm :=
by
refine ⟨convex_univ, fun x _ y _ hxy a b ha hb hab => ?_⟩
obtain ⟨x', hx''⟩ := f.surjective.exists.mp ⟨x, rfl⟩
obtain ⟨y', hy''⟩ := f.surjective.exists.mp ⟨y, rfl⟩
have hxy' : x' ≠ y' := by rw [← f.injective.ne_iff, ← hx'', ← hy'']; exact hxy
simp only [hx'', hy'', OrderIso.symm_apply_apply, gt_iff_lt]
rw [← f.lt_iff_lt, OrderIso.apply_symm_apply]
exact hf.2 (by simp : x' ∈ univ) (by simp : y' ∈ univ) hxy' ha hb hab
