convex_halfSpace_lt

Mathlib.Analysis.Convex.Basic

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

English

The half-open interval Ico(r,s) is convex in an ordered module.

Русский

Полупериод Ico(r,s) выпукл.

LaTeX

$$$\operatorname{Convex}_\mathbb{K}(\{x \in β : r \le x < s\})$$$

Lean4

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

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

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

Разделы

Аффилиация

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