feat(analysis/convex): linear image of segment (#6531)

leanprover-community · Mar 4, 2021 · 9607dbd · 9607dbd
1 parent a8d285c
commit 9607dbd
Showing 1 changed file with 3 additions and 0 deletions.
diff --git a/src/analysis/convex/basic.lean b/src/analysis/convex/basic.lean
@@ -120,6 +120,9 @@ set.ext $ λ x, mem_segment_translate a
 lemma segment_translate_image (a b c: E) : (λx, a + x) '' [b, c] = [a + b, a + c] :=
 segment_translate_preimage a b c ▸ image_preimage_eq _ $ add_left_surjective a
 
+lemma segment_image (f : E →ₗ[ℝ] F) (a b : E) : f '' [a, b] = [f a, f b] :=
+set.ext (λ x, by simp [segment_eq_image])
+
 /-! ### Convexity of sets -/
 
 /-- Convexity of sets. -/