image_openSegment — Mathlib

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]

Похожие утверждения