innerDual_singleton — Mathlib

English

The dual cone of the union of a family of sets equals the infimum (intersection) of their dual cones.

Русский

Двойной конус объединения множества равен пересечению двойных конусов каждого множества.

LaTeX

$$$\\text{innerDual}(\\bigcup_i s_i)=\\bigwedge_i innerDual(s_i)$$$

Lean4

/-- The inner dual cone of a singleton is given by the preimage of the positive cone under the
linear map `fun y ↦ ⟪x, y⟫`. -/
theorem innerDual_singleton (x : E) : innerDual ({ x } : Set E) = (positive ℝ ℝ).comap (innerSL ℝ x) := by ext; simp

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