Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2023-05-19 12:01 915591b2

View on Github →

chore(analysis/convex/cone/basic): split (#19043) Split out the inner product space material (the dual cone) from analysis/convex/cone/basic. What's left imports almost nothing, and can probably be ported immediately.

Estimated changes

deleted theorem inner_dual_cone_Union
deleted theorem inner_dual_cone_empty
deleted theorem inner_dual_cone_insert
deleted theorem inner_dual_cone_sUnion
deleted theorem inner_dual_cone_singleton
deleted theorem inner_dual_cone_union
deleted theorem inner_dual_cone_univ
deleted theorem inner_dual_cone_zero
deleted theorem is_closed_inner_dual_cone
deleted theorem mem_inner_dual_cone
deleted theorem pointed_inner_dual_cone
deleted def set.inner_dual_cone
added theorem inner_dual_cone_Union
added theorem inner_dual_cone_empty
added theorem inner_dual_cone_insert
added theorem inner_dual_cone_sUnion
added theorem inner_dual_cone_union
added theorem inner_dual_cone_univ
added theorem inner_dual_cone_zero
added theorem mem_inner_dual_cone