Zulip Chat Archive

Stream: Is there code for X?

Topic: linear image of segment


view this post on Zulip 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}
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?

view this post on Zulip Eric Wieser (Mar 01 2021 at 21:17):

docs#mem_segment_translate was the closest I could find

view this post on Zulip Eric Wieser (Mar 01 2021 at 21:18):

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

view this post on Zulip 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?

view this post on Zulip 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