Commit 2023-05-27 13:11 03406ab8

View on Github →

feat: port Analysis.Convex.Cone.Dual (#4410)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Analysis/Convex/Cone/Dual.lean

added theorem ConvexCone.hyperplane_separation_of_nonempty_of_isClosed_of_nmem

added theorem ConvexCone.innerDualCone_of_innerDualCone_eq_self

added theorem ConvexCone.pointed_of_nonempty_of_isClosed

added def Set.innerDualCone

added theorem innerDualCone_empty

added theorem innerDualCone_eq_iInter_innerDualCone_singleton

added theorem innerDualCone_iUnion

added theorem innerDualCone_insert

added theorem innerDualCone_le_innerDualCone

added theorem innerDualCone_sUnion

added theorem innerDualCone_singleton

added theorem innerDualCone_union

added theorem innerDualCone_univ

added theorem innerDualCone_zero

added theorem isClosed_innerDualCone

added theorem mem_innerDualCone

added theorem pointed_innerDualCone