vadd_openSegment — Mathlib

English

The open segment equals the image of lineMap restricted to Ioo(0,1).

Русский

Открытый сегмент равен образу lineMap ограниченному Ioo(0,1).

LaTeX

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

Lean4

@[simp]
theorem vadd_openSegment [AddTorsor G E] [VAddCommClass G E E] (a : G) (b c : E) :
    a +ᵥ openSegment 𝕜 b c = openSegment 𝕜 (a +ᵥ b) (a +ᵥ c) :=
  image_openSegment 𝕜 ⟨_, LinearMap.id, fun _ _ => vadd_comm _ _ _⟩ b c

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