nonempty

Mathlib.Analysis.Convex.Cone.Basic

URI: https://scilib.ai/kg/mathlib#ProperCone.nonempty

English

Any proper cone C in E is nonempty when viewed as a subset of E.

Русский

Любой правильный конус C в E непуст; как множество в E он содержит по крайней мере один элемент.

LaTeX

$$$(C : Set\,E) \neq \varnothing$$$

Lean4

protected theorem nonempty (C : ProperCone R E) : (C : Set E).Nonempty :=
  C.toSubmodule.nonempty

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

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

Разделы

Аффилиация

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