English
For an affine map f, the image of openSegment 𝕜 a b is the open segment between f(a) and f(b).
Русский
Для аффинного отображения f образ открытого сегмента 𝕜 a b равен открытого сегмента между f(a) и f(b).
LaTeX
$$$$ f '' openSegment_{\mathbb{K}}(a,b) = openSegment_{\mathbb{K}}(f(a), f(b)). $$$$
Lean4
@[simp]
theorem image_openSegment (f : E →ᵃ[𝕜] F) (a b : E) : f '' openSegment 𝕜 a b = openSegment 𝕜 (f a) (f b) :=
Set.ext fun x => by
simp_rw [openSegment_eq_image_lineMap, mem_image, exists_exists_and_eq_and, AffineMap.apply_lineMap]