English
x ∈ [y -[𝕜] z] iff there exist a,b ∈ 𝕜 with a,b ≥ 0, a+b>0 and x = (a/(a+b)) y + (b/(a+b)) z.
Русский
x принадлежит сегменту [y -[𝕜] z] тогда, когда существуют a,b ∈ 𝕜 такие, что a,b ≥ 0, a+b>0 и x = (a/(a+b)) y + (b/(a+b)) z.
LaTeX
$$$$ x \in [y -[\mathbb{K}] z] \iff \exists a,b:\ \ 0 \le a \land 0 \le b \land 0 < a+b \land \left(\frac{a}{a+b}\right) y + \left(\frac{b}{a+b}\right) z = x. $$$$
Lean4
theorem mem_segment_iff_div :
x ∈ [y -[𝕜] z] ↔ ∃ a b : 𝕜, 0 ≤ a ∧ 0 ≤ b ∧ 0 < a + b ∧ (a / (a + b)) • y + (b / (a + b)) • z = x :=
by
constructor
· rintro ⟨a, b, ha, hb, hab, rfl⟩
use a, b, ha, hb
simp [*]
· rintro ⟨a, b, ha, hb, hab, rfl⟩
refine ⟨a / (a + b), b / (a + b), by positivity, by positivity, ?_, rfl⟩
rw [← add_div, div_self hab.ne']
