strictConvex_iff

Mathlib.Analysis.Convex.Strict

URI: https://scilib.ai/kg/mathlib#IsOpen.strictConvex_iff

English

An open set is strictly convex if and only if it is convex.

Русский

Открытое множество строго выпукло тогда и только тогда, когда оно выпукло.

LaTeX

$$$IsOpen s \Rightarrow (StrictConvex 𝕜 s \iff Convex 𝕜 s)$$$

Lean4

theorem strictConvex_iff (h : IsOpen s) : StrictConvex 𝕜 s ↔ Convex 𝕜 s :=
  ⟨StrictConvex.convex, Convex.strictConvex_of_isOpen h⟩

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

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

Разделы

Аффилиация

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