𝕜 : Type u_1
𝕝 : Type ?u.141875
E : Type u_2
ι : Sort ?u.141881
κ : ι → Sort ?u.141886
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 : 𝕜
x : E
a : 𝕜
ha : 1 ≤ ‖a‖
⊢ x ∈ a • univ
𝕜 : Type u_1
𝕝 : Type ?u.141875
E : Type u_2
ι : Sort ?u.141881
κ : ι → Sort ?u.141886
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 : 𝕜
⊢ Absorbent 𝕜 univ
refine' fun x => ⟨1, zero_lt_one, fun a ha => _⟩
𝕜 : Type u_1
𝕝 : Type ?u.141875
E : Type u_2
ι : Sort ?u.141881
κ : ι → Sort ?u.141886
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 : 𝕜
x : E
a : 𝕜
ha : 1 ≤ ‖a‖
⊢ x ∈ univ
𝕜 : Type u_1
𝕝 : Type ?u.141875
E : Type u_2
ι : Sort ?u.141881
κ : ι → Sort ?u.141886
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 : 𝕜
x : E
a : 𝕜
ha : 1 ≤ ‖a‖
⊢ x ∈ a • univ
rw [smul_set_univ₀ (norm_pos_iff.1 <| zero_lt_one.trans_le ha)]
no goals
𝕜 : Type u_1
𝕝 : Type ?u.141875
E : Type u_2
ι : Sort ?u.141881
κ : ι → Sort ?u.141886
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 : 𝕜
x : E
a : 𝕜
ha : 1 ≤ ‖a‖
⊢ x ∈ univ
exact trivial