𝕜 : Type u_1
E : Type ?u.291676
F : Type ?u.291679
G : Type ?u.291682
ι : Type ?u.291685
π : ι → Type ?u.291690
inst✝ : LinearOrderedField 𝕜
x y z : 𝕜
h : x ≤ y
⊢ z ∈ [x-[𝕜]y] ↔ ∃ a b, 0 ≤ a ∧ 0 ≤ b ∧ a + b = 1 ∧ a * x + b * y = z
𝕜 : Type u_1
E : Type ?u.291676
F : Type ?u.291679
G : Type ?u.291682
ι : Type ?u.291685
π : ι → Type ?u.291690
inst✝ : LinearOrderedField 𝕜
x y z : 𝕜
h : x ≤ y
⊢ z ∈ Icc x y ↔ ∃ a b, 0 ≤ a ∧ 0 ≤ b ∧ a + b = 1 ∧ a * x + b * y = z
rw [← segment_eq_Icc h]
𝕜 : Type u_1
E : Type ?u.291676
F : Type ?u.291679
G : Type ?u.291682
ι : Type ?u.291685
π : ι → Type ?u.291690
inst✝ : LinearOrderedField 𝕜
x y z : 𝕜
h : x ≤ y
⊢ z ∈ [x-[𝕜]y] ↔ ∃ a b _h _h _h, a * x + b * y = z
𝕜 : Type u_1
E : Type ?u.291676
F : Type ?u.291679
G : Type ?u.291682
ι : Type ?u.291685
π : ι → Type ?u.291690
inst✝ : LinearOrderedField 𝕜
x y z : 𝕜
h : x ≤ y
⊢ z ∈ [x-[𝕜]y] ↔ ∃ a b, 0 ≤ a ∧ 0 ≤ b ∧ a + b = 1 ∧ a * x + b * y = z
simp_rw [← exists_prop]
no goals
𝕜 : Type u_1
E : Type ?u.291676
F : Type ?u.291679
G : Type ?u.291682
ι : Type ?u.291685
π : ι → Type ?u.291690
inst✝ : LinearOrderedField 𝕜
x y z : 𝕜
h : x ≤ y
⊢ z ∈ [x-[𝕜]y] ↔ ∃ a b _h _h _h, a * x + b * y = z
rfl