mem_bot

Mathlib.Analysis.Convex.Cone.Basic

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

English

If the ambient space E is T1, then the bottom cone equals {0} in E.

Русский

Если пространство E является T1, то нижний конус равен {0}.

LaTeX

$$x ∈ ⊥ ⇔ x = 0$$

Lean4

theorem mem_bot : x ∈ (⊥ : ProperCone R E) ↔ x = 0 :=
  .rfl

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

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

Разделы

Аффилиация

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