Commit 2022-08-09 14:16 1a51c706

feat(analysis/convex/cone): lemmas about inner_dual_cone of unions (#15836) This discards the proof in #15639 and replaces it with a more general strategy and some auxiliary lemmas. This includes an insert lemma for consistency with submodule.span_insert, even though it follows trivially from the union lemma.