convex_halfSpace_gt

Mathlib.Analysis.Convex.Basic

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

English

For a linear map f, the strict half-space {w | r < f(w)} is convex.

Русский

Для линейного отображения $f$ множество {w | r < f(w)} выпукло.

LaTeX

$$$\operatorname{Convex}_\mathbb{K}(\{w \in E : r < f(w)\})$$$

Lean4

theorem convex_halfSpace_gt {f : E → β} (h : IsLinearMap 𝕜 f) (r : β) : Convex 𝕜 {w | r < f w} :=
  (convex_Ioi r).is_linear_preimage h

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

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

Разделы

Аффилиация

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