concaveOn_id

Mathlib.Analysis.Convex.Function

URI: https://scilib.ai/kg/mathlib#concaveOn_id

English

If S is convex, then the identity map is concave on S.

Русский

Если S выпукло, то отображение на S, identically, является конкавным.

LaTeX

$$$$ \\operatorname{ConcaveOn}_{\\mathsf{𝕜}}(S,\\mathrm{id}) \\;\\text{ when } \\operatorname{Convex}_{\\mathsf{𝕜}}(S). $$$$

Lean4

theorem concaveOn_id {s : Set β} (hs : Convex 𝕜 s) : ConcaveOn 𝕜 s _root_.id :=
  ⟨hs, by
    intros
    rfl⟩

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru