linear image of segment

Stream: Is there code for X?

[Bhavik Mehta]

import analysis.convex.basic

open linear_map
universes u v

variables {E : Type u} {F : Type v}
variables [add_comm_group E] [vector_space ℝ E] [add_comm_group F] [vector_space ℝ F]

lemma segment_image (f : E →ₗ[ℝ] F) (a b : E) : f '' segment a b = segment (f a) (f b) :=
begin

end

Is something like this in mathlib somewhere?

[Eric Wieser]

docs#mem_segment_translate was the closest I could find

[Eric Wieser]

Which I guess you want to generalize from (+ a) to any affine map?

[Adam Topaz]

Shouldn't there be a lemma saying that an affine map sends segments to segments, and something which constructs an affine map out of a linear map?

[Bhavik Mehta]

Turned out it just has a one line proof - perhaps it should be there for affine maps though