English
If s is balanced with respect to 𝕝 and ‖a‖ ≤ ‖b‖, then the scaled set a · s is contained in b · s.
Русский
Если s сбалансировано относительно 𝕝 и ‖a‖ ≤ ‖b‖, то множество a · s содержится в b · s.
LaTeX
$$$\\\\text{Balanced } 𝕝\\, s \\\\rightarrow\\\\forall {a,b} \\\\in 𝕝, \\\\|a\\| \\\\le \\\\|b\\\\| \\\\Rightarrow \\\\ a \\\\cdot s \\\\subseteq b \\\\cdot s$$$
Lean4
/-- Scalar multiplication (by possibly different types) of a balanced set is monotone. -/
theorem smul_mono (hs : Balanced 𝕝 s) {a : 𝕝} (h : ‖a‖ ≤ ‖b‖) : a • s ⊆ b • s :=
by
obtain rfl | hb := eq_or_ne b 0
· rw [norm_zero, norm_le_zero_iff] at h
simp only [h, ← image_smul, zero_smul, Subset.rfl]
·
calc
a • s = b • (b⁻¹ • a) • s := by rw [smul_assoc, smul_inv_smul₀ hb]
_ ⊆ b • s :=
smul_set_mono <|
hs _ <| by
rw [norm_smul, norm_inv, ← div_eq_inv_mul]
exact div_le_one_of_le₀ h (norm_nonneg _)
