mem_segment_sub_add — Mathlib

English

Membership of x in [x−y -[𝕜] x+y] holds under invertible 2 and standard operations.

Русский

При инвертируемости двойки и стандартных операциях x ∈ [x−y -[𝕜] x+y].

LaTeX

$$$$ x \in [x -[\mathbb{K}] y -[\mathbb{K}] x + y]. $$$$

Lean4

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

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