𝕜 : Type u_1
E : Type ?u.294082
F : Type ?u.294085
G : Type ?u.294088
ι : Type ?u.294091
π : ι → Type ?u.294096
inst✝ : LinearOrderedField 𝕜
x y z : 𝕜
h : x < y
⊢ z ∈ openSegment 𝕜 x y ↔ ∃ a b, 0 < a ∧ 0 < b ∧ a + b = 1 ∧ a * x + b * y = z
𝕜 : Type u_1
E : Type ?u.294082
F : Type ?u.294085
G : Type ?u.294088
ι : Type ?u.294091
π : ι → Type ?u.294096
inst✝ : LinearOrderedField 𝕜
x y z : 𝕜
h : x < y
⊢ z ∈ Ioo x y ↔ ∃ a b, 0 < a ∧ 0 < b ∧ a + b = 1 ∧ a * x + b * y = z
rw [← openSegment_eq_Ioo h]
𝕜 : Type u_1
E : Type ?u.294082
F : Type ?u.294085
G : Type ?u.294088
ι : Type ?u.294091
π : ι → Type ?u.294096
inst✝ : LinearOrderedField 𝕜
x y z : 𝕜
h : x < y
⊢ z ∈ openSegment 𝕜 x y ↔ ∃ a b _h _h _h, a * x + b * y = z
𝕜 : Type u_1
E : Type ?u.294082
F : Type ?u.294085
G : Type ?u.294088
ι : Type ?u.294091
π : ι → Type ?u.294096
inst✝ : LinearOrderedField 𝕜
x y z : 𝕜
h : x < y
⊢ z ∈ openSegment 𝕜 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.294082
F : Type ?u.294085
G : Type ?u.294088
ι : Type ?u.294091
π : ι → Type ?u.294096
inst✝ : LinearOrderedField 𝕜
x y z : 𝕜
h : x < y
⊢ z ∈ openSegment 𝕜 x y ↔ ∃ a b _h _h _h, a * x + b * y = z
rfl