mem_dual — Mathlib

English

The dual of a pointed cone with respect to a pairing is a closed subcone of the dual space.

Русский

Дуал указательного конуса относительно данного биективного отображения является замкнутым подпоконусом двойственного пространства.

LaTeX

$$dual p s ∈ ProperCone 𝕜 N with s ⊆ M$$

Lean4

@[simp]
theorem mem_dual : y ∈ dual p s ↔ ∀ ⦃x⦄, x ∈ s → 0 ≤ p x y :=
  .rfl

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