English
If f is strictly convex and an order isomorphism, then its inverse f^{-1} is strictly concave.
Русский
Если f строго выпукла и является отображением, сохраняющим порядок, то её обратная функция строго вогнутая.
LaTeX
$$$$\\text{If } f:\\alpha \\to \\beta \\text{ is an order isomorphism and } f \\text{ is strictly convex on } \\mathsf{univ}, \\text{ then } f^{-1}:\\beta \\to \\alpha \\text{ is strictly concave on } \\mathsf{univ}.$$$$
Lean4
theorem strictConcaveOn_symm (f : α ≃o β) (hf : StrictConvexOn 𝕜 univ f) : StrictConcaveOn 𝕜 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
