English
Let K be a convex body in a real vector space V with 0 ∈ K. If a,b ∈ ℝ≥0 and a ≤ b, then a·K ⊆ b·K.
Русский
Пусть K — выпуклое тело в вещественном векторном пространстве V и 0 принадлежит K. Если a,b ∈ ℝ≥0 и a ≤ b, то a·K ⊆ b·K.
LaTeX
$$$\\text{Let }K\\text{ be a convex body in }V\\text{ with }0\\in K.\\; \\text{For }a,b\\in\\mathbb{R}_{\\ge 0},\\ a\\le b\\ \\Rightarrow\\ aK\\subseteq bK.$$$
Lean4
theorem smul_le_of_le (K : ConvexBody V) (h_zero : 0 ∈ K) {a b : ℝ≥0} (h : a ≤ b) : a • K ≤ b • K :=
by
rw [← SetLike.coe_subset_coe, coe_smul', coe_smul']
obtain rfl | ha := eq_zero_or_pos a
· rw [Set.zero_smul_set K.nonempty, Set.zero_subset]
exact Set.mem_smul_set.mpr ⟨0, h_zero, smul_zero _⟩
· intro x hx
obtain ⟨y, hy, rfl⟩ := Set.mem_smul_set.mp hx
rw [← Set.mem_inv_smul_set_iff₀ ha.ne', smul_smul]
refine Convex.mem_smul_of_zero_mem K.convex h_zero hy (?_ : 1 ≤ a⁻¹ * b)
rwa [le_inv_mul_iff₀ ha, mul_one]
