𝕜 : Type u_1
𝕝 : Type ?u.76198
E : Type u_2
ι : Sort ?u.76204
κ : ι → Sort ?u.76209
inst✝⁶ : NormedField 𝕜
inst✝⁵ : NormedRing 𝕝
inst✝⁴ : NormedSpace 𝕜 𝕝
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
inst✝¹ : SMulWithZero 𝕝 E
inst✝ : IsScalarTower 𝕜 𝕝 E
s t u v A B : Set E
x✝ : E
a✝ b : 𝕜
hA : Balanced 𝕜 A
a : 𝕜
ha : 1 ≤ ‖a‖
x : E
hx : x ∈ A
⊢ x ∈ a • A
𝕜 : Type u_1
𝕝 : Type ?u.76198
E : Type u_2
ι : Sort ?u.76204
κ : ι → Sort ?u.76209
inst✝⁶ : NormedField 𝕜
inst✝⁵ : NormedRing 𝕝
inst✝⁴ : NormedSpace 𝕜 𝕝
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
inst✝¹ : SMulWithZero 𝕝 E
inst✝ : IsScalarTower 𝕜 𝕝 E
s t u v A B : Set E
x : E
a b : 𝕜
hA : Balanced 𝕜 A
⊢ Absorbs 𝕜 A A
refine' ⟨1, zero_lt_one, fun a ha x hx => _⟩
𝕜 : Type u_1
𝕝 : Type ?u.76198
E : Type u_2
ι : Sort ?u.76204
κ : ι → Sort ?u.76209
inst✝⁶ : NormedField 𝕜
inst✝⁵ : NormedRing 𝕝
inst✝⁴ : NormedSpace 𝕜 𝕝
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
inst✝¹ : SMulWithZero 𝕝 E
inst✝ : IsScalarTower 𝕜 𝕝 E
s t u v A B : Set E
x✝ : E
a✝ b : 𝕜
hA : Balanced 𝕜 A
a : 𝕜
ha : 1 ≤ ‖a‖
x : E
hx : x ∈ A
⊢ a⁻¹ • x ∈ A
𝕜 : Type u_1
𝕝 : Type ?u.76198
E : Type u_2
ι : Sort ?u.76204
κ : ι → Sort ?u.76209
inst✝⁶ : NormedField 𝕜
inst✝⁵ : NormedRing 𝕝
inst✝⁴ : NormedSpace 𝕜 𝕝
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
inst✝¹ : SMulWithZero 𝕝 E
inst✝ : IsScalarTower 𝕜 𝕝 E
s t u v A B : Set E
x✝ : E
a✝ b : 𝕜
hA : Balanced 𝕜 A
a : 𝕜
ha : 1 ≤ ‖a‖
x : E
hx : x ∈ A
⊢ x ∈ a • A
rw [mem_smul_set_iff_inv_smul_mem₀ (norm_pos_iff.1 <| zero_lt_one.trans_le ha)]
𝕜 : Type u_1
𝕝 : Type ?u.76198
E : Type u_2
ι : Sort ?u.76204
κ : ι → Sort ?u.76209
inst✝⁶ : NormedField 𝕜
inst✝⁵ : NormedRing 𝕝
inst✝⁴ : NormedSpace 𝕜 𝕝
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
inst✝¹ : SMulWithZero 𝕝 E
inst✝ : IsScalarTower 𝕜 𝕝 E
s t u v A B : Set E
x✝ : E
a✝ b : 𝕜
hA : Balanced 𝕜 A
a : 𝕜
ha : 1 ≤ ‖a‖
x : E
hx : x ∈ A
⊢ ‖a⁻¹‖ ≤ 1
𝕜 : Type u_1
𝕝 : Type ?u.76198
E : Type u_2
ι : Sort ?u.76204
κ : ι → Sort ?u.76209
inst✝⁶ : NormedField 𝕜
inst✝⁵ : NormedRing 𝕝
inst✝⁴ : NormedSpace 𝕜 𝕝
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
inst✝¹ : SMulWithZero 𝕝 E
inst✝ : IsScalarTower 𝕜 𝕝 E
s t u v A B : Set E
x✝ : E
a✝ b : 𝕜
hA : Balanced 𝕜 A
a : 𝕜
ha : 1 ≤ ‖a‖
x : E
hx : x ∈ A
⊢ a⁻¹ • x ∈ A
refine' hA a⁻¹ _ (smul_mem_smul_set hx)
𝕜 : Type u_1
𝕝 : Type ?u.76198
E : Type u_2
ι : Sort ?u.76204
κ : ι → Sort ?u.76209
inst✝⁶ : NormedField 𝕜
inst✝⁵ : NormedRing 𝕝
inst✝⁴ : NormedSpace 𝕜 𝕝
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
inst✝¹ : SMulWithZero 𝕝 E
inst✝ : IsScalarTower 𝕜 𝕝 E
s t u v A B : Set E
x✝ : E
a✝ b : 𝕜
hA : Balanced 𝕜 A
a : 𝕜
ha : 1 ≤ ‖a‖
x : E
hx : x ∈ A
⊢ ‖a‖⁻¹ ≤ 1
𝕜 : Type u_1
𝕝 : Type ?u.76198
E : Type u_2
ι : Sort ?u.76204
κ : ι → Sort ?u.76209
inst✝⁶ : NormedField 𝕜
inst✝⁵ : NormedRing 𝕝
inst✝⁴ : NormedSpace 𝕜 𝕝
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
inst✝¹ : SMulWithZero 𝕝 E
inst✝ : IsScalarTower 𝕜 𝕝 E
s t u v A B : Set E
x✝ : E
a✝ b : 𝕜
hA : Balanced 𝕜 A
a : 𝕜
ha : 1 ≤ ‖a‖
x : E
hx : x ∈ A
⊢ ‖a⁻¹‖ ≤ 1
rw [norm_inv]
no goals
𝕜 : Type u_1
𝕝 : Type ?u.76198
E : Type u_2
ι : Sort ?u.76204
κ : ι → Sort ?u.76209
inst✝⁶ : NormedField 𝕜
inst✝⁵ : NormedRing 𝕝
inst✝⁴ : NormedSpace 𝕜 𝕝
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
inst✝¹ : SMulWithZero 𝕝 E
inst✝ : IsScalarTower 𝕜 𝕝 E
s t u v A B : Set E
x✝ : E
a✝ b : 𝕜
hA : Balanced 𝕜 A
a : 𝕜
ha : 1 ≤ ‖a‖
x : E
hx : x ∈ A
⊢ ‖a‖⁻¹ ≤ 1
exact inv_le_one ha