English
Let x be a point in H and s a subset of H. Then the dual cone of insert x s equals the intersection of the dual cone of the singleton {x} with the dual cone of s: (insert x s).innerDualCone = {x}.innerDualCone ∩ s.innerDualCone.
Русский
Пусть x ∈ H и s ⊆ H. Тогда дуальный конус вставки x в s равен пересечению дуального конуса {x} и дуального конуса s: (insert x s).innerDualCone = {x}.innerDualCone ∩ s.innerDualCone.
LaTeX
$$$ (\\operatorname{insert} x\, s).innerDualCone = (\\{x\\}.innerDualCone) \\cap (s.innerDualCone) $$$
Lean4
@[deprecated ProperCone.innerDual_insert (since := "2025-07-06")]
theorem innerDualCone_insert (x : H) (s : Set H) :
(insert x s).innerDualCone = Set.innerDualCone { x } ⊓ s.innerDualCone := by rw [insert_eq, innerDualCone_union]
