English
Let s and t be subsets of a real inner product space H. Then the dual cone of their union equals the intersection of the dual cones: (s ∪ t).innerDualCone = s.innerDualCone ∩ t.innerDualCone.
Русский
Пусть s и t — подмножества вещественного пространства с альтернативным скалярным произведением H. Тогда дуальный конус объединения равен пересечению дуальных конусов: (s ∪ t).innerDualCone = s.innerDualCone ∩ t.innerDualCone.
LaTeX
$$$ (s \\cup t).innerDualCone = s.innerDualCone \\cap t.innerDualCone $$$
Lean4
@[deprecated ProperCone.innerDual_union (since := "2025-07-06")]
theorem innerDualCone_union (s t : Set H) : (s ∪ t).innerDualCone = s.innerDualCone ⊓ t.innerDualCone :=
le_antisymm (le_inf (fun _ hx _ hy => hx _ <| Or.inl hy) fun _ hx _ hy => hx _ <| Or.inr hy) fun _ hx _ =>
Or.rec (hx.1 _) (hx.2 _)
