convex_hull_image

Stream: general

[Yaël Dillies]

We have both

lemma linear_map.image_convex_hull (f : E →ₗ[𝕜] F) :
  f '' (convex_hull 𝕜 s) = convex_hull 𝕜 (f '' s) := sorry

and

lemma linear_map.convex_hull_image (f : E →ₗ[𝕜] F) (s : set E) :
  convex_hull 𝕜 (f '' s) = f '' convex_hull 𝕜 s :=

Which one do we want to keep?

[Yaël Dillies]

I'd say f '' convex_hull 𝕜 s is simpler than convex_hull 𝕜 (f '' s), but that's arguable.

[Johan Commelin]

image_convex_hull seems to be used 3 times, while convex_hull_image is used 2 times.

[Eric Wieser]

If we can't decide which is worth keeping, we could at least put them next to each other in the same file

[Yaël Dillies]

Johan Commelin said:

image_convex_hull seems to be used 3 times, while convex_hull_image is used 2 times.

The VScode search found me none of those :sad:

[Johan Commelin]

grep power!

[Yaël Dillies]

I can't handle that much power!