convex_halfSpace_le

Mathlib.Analysis.Convex.Basic

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

English

For any linear map f, the sublevel set {w ∈ E | f(w) ≤ r} is convex.

Русский

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

LaTeX

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

Lean4

theorem convex_halfSpace_le {f : E → β} (h : IsLinearMap 𝕜 f) (r : β) : Convex 𝕜 {w | f w ≤ r} :=
  (convex_Iic r).is_linear_preimage h

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

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

Разделы

Аффилиация

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