mem_openSegment_translate — Mathlib

English

Translation by a fixed vector preserves open segment membership similarly.

Русский

Сдвиг сохраняет членство в открытом сегменте аналогично.

LaTeX

$$$$ a + x \in openSegment_{\mathbb{K}}(a+b,a+c) \iff x \in openSegment_{\mathbb{K}}(b,c). $$$$

Lean4

@[simp]
theorem mem_openSegment_translate (a : E) {x b c : E} : a + x ∈ openSegment 𝕜 (a + b) (a + c) ↔ x ∈ openSegment 𝕜 b c :=
  by simp_rw [← vadd_eq_add, ← vadd_openSegment, vadd_mem_vadd_set_iff]

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