## Stream: Is there code for X?

### Topic: linear image of segment

#### Bhavik Mehta (Mar 01 2021 at 20:32):

import analysis.convex.basic

open linear_map
universes u v

variables {E : Type u} {F : Type v}

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 (Mar 01 2021 at 21:17):

docs#mem_segment_translate was the closest I could find

#### Eric Wieser (Mar 01 2021 at 21:18):

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

#### Adam Topaz (Mar 01 2021 at 21:20):

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 (Mar 01 2021 at 23:09):

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

Last updated: May 16 2021 at 05:21 UTC