anti

Mathlib.Geometry.Convex.Cone.Basic

URI: https://scilib.ai/kg/mathlib#ConvexCone.Salient.anti

English

Equivalently, C.Pointed holds exactly when 0 ∈ C.

Русский

Эквивалентно: C.Pointed выполняется тогда, когда 0 ∈ C.

LaTeX

$$C.Pointed \iff (0 \in C)$$

Lean4

theorem anti (h : C₂ ≤ C₁) : C₁.Salient → C₂.Salient := fun hS x hxT hx hnT => hS x (h hxT) hx (h hnT)

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

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

Разделы

Аффилиация

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