Repository navigation
Conversation
…Homogenization.lean Co-authored-by: M. Winter <112132359+martinwintermath@users.noreply.github.com>
| @[ext] theorem ext {F₁ F₂ : Face P} (h : ∀ x, x ∈ F₁ ↔ x ∈ F₂) : F₁ = F₂ := SetLike.ext h | ||
|
|
||
| @[simp] theorem coe_eq_toConvexSet_coe {F : Face P} : (F : Set M) = F.toConvexSet := | ||
| SetLike.ext'_iff.mp rfl | ||
|
|
There was a problem hiding this comment.
Why are these no longer needed? :o
There was a problem hiding this comment.
the first should be generated by @[ext] annotation on structure Face, the second because Face does no longer coerce to ConvexSet but to Set now
| structure Face (P : ConvexSet R M) extends toConvexSet : ConvexSet R M where | ||
| isFaceOf : IsFaceOf toConvexSet P | ||
| @[ext] | ||
| structure Face {p : Set M} (P : IsConvexSet R p) where |
There was a problem hiding this comment.
| structure Face {p : Set M} (P : IsConvexSet R p) where | |
| structure Face {p : Set M} where |
This seems unneccesary.
| namespace IsConvexSet | ||
|
|
||
| /- NOTE: maybe this should be defined on `Set` instead of `ConvexSet`. -/ | ||
| /-- A face of a convex set `P`. Represents the face lattice of `P`. -/ |
There was a problem hiding this comment.
| /-- A face of a convex set `P`. Represents the face lattice of `P`. -/ | |
| /-- A face of a set `P`. This type also represents the face lattice of `P`. -/ |
|
|
||
| variable (ℋ : Affine.IsHomogenization R A W) | ||
|
|
||
| /-- The homogenization cone of a convex set in an affine space. -/ |
There was a problem hiding this comment.
| /-- The homogenization cone of a convex set in an affine space. -/ | |
| /-- The homogenization cone of a set in an affine space. -/ |
| toFun K := ⟨_, K.homogenize_le_weight_positive _⟩ | ||
| invFun C := dehomogenize ℋ C.1 | ||
| left_inv K := dehomogenize_homogenize _ K | ||
| def homogenizeOrderEquiv : {s : Set A // IsConvexSet R s} ≃o Set.Iic ℋ.weight.positive where |
There was a problem hiding this comment.
This order equiv is a valid use case of ConvexSet, it should not be rewritten without it.
| @@ -0,0 +1,260 @@ | |||
| /- | |||
There was a problem hiding this comment.
Cant his file be a separate PR? (updated to current mathlib PR version).
|
|
||
| public import Polyhedral.Mathlib.Geometry.Convex.ConvexSpace.Polytope.Lattice | ||
| public import Polyhedral.Mathlib.Geometry.Convex.ConvexSpace.Polyhedron.Basic | ||
| public import Polyhedral.Mathlib.Geometry.Convex.ConvexSpace.Set.Lattice |
There was a problem hiding this comment.
Do we know why this import became necessary?
|
|
||
| @[simp] theorem mk_eq {s h} : (⟨s, h⟩ : Polytope R X) = s := by ext; simp | ||
|
|
||
| instance : Coe (Polytope R X) (ConvexSet R X) where |
There was a problem hiding this comment.
Don't delete this.
|
|
||
| instance : IsConcreteNeg (Polytope R X) X := ⟨fun _ => rfl⟩ | ||
|
|
||
| instance : InvolutiveNeg (ConvexSet R X) := .ofSetLike .. |
There was a problem hiding this comment.
Don't delete this, but ConvexSet should have been Polytope (apparently this was an oversight in the earlier version).
2 participants
attempting to remove bundled convex sets. wip, some renaming and moving of lemmas needs to be done. wdyt?
IsFaceOfis just extreme subsetsFacerequires both face and faced set to be convex (otherwise its not very interesting and we'd need to define this lattice anyways for homogenization)homogenizeanddehomognizeare both defined on general sets. in particular, we need the assumption of convexity fordehomogenize ℋ (homogenize ℋ P) = P. the order equivalence becomes