openSegment_eq_image' — Mathlib

English

The open segment can also be written as the image of the map θ ↦ x + θ(y − x) from θ ∈ (0,1).

Русский

Открытый сегмент можно записать как образ отображения θ ↦ x + θ(y − x) при θ ∈ (0,1).

LaTeX

$$$$ openSegment_{\mathbb{K}}(x,y) = \{ x + \theta (y - x) : \theta \in (0,1) \}. $$$$

Lean4

theorem openSegment_eq_image' (x y : E) : openSegment 𝕜 x y = (fun θ : 𝕜 => x + θ • (y - x)) '' Ioo (0 : 𝕜) 1 :=
  by
  convert openSegment_eq_image 𝕜 x y using 2
  simp only [smul_sub, sub_smul, one_smul]
  abel

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