Commit 2023-06-09 01:23 74f1d619

View on Github →

feat(analysis/convex/cone/proper): define proper cone (#18913) Part of #16266 We define proper cones as nonempty, closed cones and define duals. Next todo: Prove Farkas' lemma from #19008

Estimated changes

Modified src/analysis/convex/cone/proper.lean

added theorem convex_cone.closure_eq

modified theorem convex_cone.coe_closure

added theorem proper_cone.coe_dual

added theorem proper_cone.coe_map

added theorem proper_cone.coe_zero

added def proper_cone.dual

added theorem proper_cone.dual_dual

added theorem proper_cone.ext'

added theorem proper_cone.ext

added theorem proper_cone.map_id

added theorem proper_cone.mem_coe

added theorem proper_cone.mem_dual

added theorem proper_cone.mem_map

added theorem proper_cone.mem_zero

added theorem proper_cone.pointed_zero

added theorem proper_cone.to_convex_cone_eq_coe

added structure proper_cone