Mathlib v3 is deprecated. Go to Mathlib v4

Theorem convex_cone.hyperplane_separation_of_nonempty_of_is_closed_of_nmem

Modification history

2023-05-19 12:01
src/analysis/convex/cone/basic.lean
chore(analysis/convex/cone/basic): split (#19043) …
Modified convex_cone.hyperplane_separation_of_nonempty_of_is_closed_of_nmemView on Github →
2022-08-25 03:05
src/analysis/convex/cone.lean
feat(analysis/convex/cone): add `inner_dual_cone_of_inner_dual_cone_eq_self` for nonempty, closed, convex cones (#15637) …
Added convex_cone.hyperplane_separation_of_nonempty_of_is_closed_of_nmemView on Github →