English
If hs is balanced and ha remains, then a smul_mem_mono gives that from ha ∈ s, and ‖b‖ ≤ ‖a‖, we get b · x ∈ s.
Русский
Если hs сбалансировано и ha сохраняется, то из ha ∈ s и ‖b‖ ≤ ‖a‖ следует b · x ∈ s.
LaTeX
$$$\\text{Balanced } 𝕝\\ s \\land \\ ha \\in s \\Rightarrow \\ b \\cdot x \\in s$ при условии $\\|b\\| \\le \\|a\\|$$$
Lean4
theorem smul_mem_mono [SMulCommClass 𝕝 𝕜 E] (hs : Balanced 𝕝 s) {b : 𝕝} (ha : a • x ∈ s) (hba : ‖b‖ ≤ ‖a‖) :
b • x ∈ s := by
rcases eq_or_ne a 0 with rfl | ha₀
· simp_all
·
calc
(a⁻¹ • b) • a • x ∈ s := by
refine hs.smul_mem ?_ ha
rw [norm_smul, norm_inv, ← div_eq_inv_mul]
exact div_le_one_of_le₀ hba (norm_nonneg _)
(a⁻¹ • b) • a • x = b • x := by rw [smul_comm, smul_assoc, smul_inv_smul₀ ha₀]
