𝕜 : Type u_1
E : Type u_2
F : Type ?u.56571
G : Type ?u.56574
inst✝² : LinearOrderedField 𝕜
inst✝¹ : OrderedAddCommGroup E
inst✝ : Module 𝕜 E
S : ConvexCone 𝕜 E
h : ∀ (x y : E), x ≤ y ↔ y - x ∈ S
x y : E
z : 𝕜
xy : x < y
hz : 0 < z
⊢ z • x ≤ z • y
𝕜 : Type u_1
E : Type u_2
F : Type ?u.56571
G : Type ?u.56574
inst✝² : LinearOrderedField 𝕜
inst✝¹ : OrderedAddCommGroup E
inst✝ : Module 𝕜 E
S : ConvexCone 𝕜 E
h : ∀ (x y : E), x ≤ y ↔ y - x ∈ S
⊢ ∀ ⦃a b : E⦄ ⦃c : 𝕜⦄, a < b → 0 < c → c • a ≤ c • b
intro x y z xy hz
𝕜 : Type u_1
E : Type u_2
F : Type ?u.56571
G : Type ?u.56574
inst✝² : LinearOrderedField 𝕜
inst✝¹ : OrderedAddCommGroup E
inst✝ : Module 𝕜 E
S : ConvexCone 𝕜 E
h : ∀ (x y : E), x ≤ y ↔ y - x ∈ S
x y : E
z : 𝕜
xy : x < y
hz : 0 < z
⊢ z • (y - x) ∈ S
𝕜 : Type u_1
E : Type u_2
F : Type ?u.56571
G : Type ?u.56574
inst✝² : LinearOrderedField 𝕜
inst✝¹ : OrderedAddCommGroup E
inst✝ : Module 𝕜 E
S : ConvexCone 𝕜 E
h : ∀ (x y : E), x ≤ y ↔ y - x ∈ S
x y : E
z : 𝕜
xy : x < y
hz : 0 < z
⊢ z • x ≤ z • y
rw [h (z • x) (z • y), ← smul_sub z y x]
no goals
𝕜 : Type u_1
E : Type u_2
F : Type ?u.56571
G : Type ?u.56574
inst✝² : LinearOrderedField 𝕜
inst✝¹ : OrderedAddCommGroup E
inst✝ : Module 𝕜 E
S : ConvexCone 𝕜 E
h : ∀ (x y : E), x ≤ y ↔ y - x ∈ S
x y : E
z : 𝕜
xy : x < y
hz : 0 < z
⊢ z • (y - x) ∈ S
exact smul_mem S hz ((h x y).mp xy.le)