starConvex_compl_Ici

Mathlib.Analysis.Convex.Star

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

← MathLib Explorer

English

If x<y then the complement of [y, ∞) is star-convex at x.

Русский

Если x<y, то дополнение множества [y, ∞) звёздочно выпукло относительно x.

LaTeX

$$$\\text{starConvex}_{\\mathbb{K}}(x, [y,\\infty)^{c})$ при $x

Lean4

/-- If `x < y`, then `(Set.Ici y)ᶜ` is star convex at `x`. -/
theorem starConvex_compl_Ici (h : x < y) : StarConvex 𝕜 x (Ici y)ᶜ :=
  starConvex_compl_Iic (E := Eᵒᵈ) h

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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