mem_segment_add_sub

Mathlib.Analysis.Convex.Segment

URI: https://scilib.ai/kg/mathlib#mem_segment_add_sub

← MathLib Explorer

English

The preimage under translation of a segment equals another segment.

Русский

Предобраз под сдвигом сегмента равен другому сегменту.

LaTeX

$$$$ (\lambda x. a+x)^{-1'}([a+b -[\mathbb{K}] a+c]) = [b -[\mathbb{K}] c]. $$$$

Lean4

theorem mem_segment_add_sub [Invertible (2 : 𝕜)] (x y : E) : x ∈ [x + y -[𝕜] x - y] :=
  by
  convert midpoint_mem_segment (𝕜 := 𝕜) (x + y) (x - y)
  rw [midpoint_add_sub]

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

Научная платформа российской исследовательской школы.

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru