mem_openSegment_iff_div — Mathlib

English

Let 𝕜 be a semifield and E a 𝕜-vector space. For x, y, z ∈ E, x lies in the open segment between y and z if and only if there exist a, b ∈ 𝕜 with a > 0 and b > 0 such that x = (a/(a+b)) · y + (b/(a+b)) · z.

Русский

Пусть 𝕜 – полевой полюс, E – векторное пространство над 𝕜. Пусть x, y, z ∈ E. Тогда x принадлежит открытому сегменту между y и z тогда и только тогда существуют a, b ∈ 𝕜 такие, что a > 0, b > 0 и x = (a/(a+b))·y + (b/(a+b))·z.

LaTeX

$$$ x \in openSegment_{\mathbb{k}}\; y\; z \iff \exists a,b \in \mathbb{k},\ 0

Lean4

theorem mem_openSegment_iff_div :
    x ∈ openSegment 𝕜 y z ↔ ∃ a b : 𝕜, 0 < a ∧ 0 < b ∧ (a / (a + b)) • y + (b / (a + b)) • z = x :=
  by
  constructor
  · rintro ⟨a, b, ha, hb, hab, rfl⟩
    use a, b, ha, hb
    rw [hab, div_one, div_one]
  · rintro ⟨a, b, ha, hb, rfl⟩
    have hab : 0 < a + b := add_pos' ha hb
    refine ⟨a / (a + b), b / (a + b), by positivity, by positivity, ?_, rfl⟩
    rw [← add_div, div_self hab.ne']

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