𝕜 : Type u_1
𝕝 : Type ?u.204287
E : Type u_2
ι : Sort ?u.204293
κ : ι → Sort ?u.204298
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s : Set E
⊢ Absorbs 𝕜 s 0 → 0 ∈ s
𝕜 : Type u_1
𝕝 : Type ?u.204287
E : Type u_2
ι : Sort ?u.204293
κ : ι → Sort ?u.204298
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s : Set E
⊢ Absorbs 𝕜 s 0 ↔ 0 ∈ s
refine' ⟨_, fun h => ⟨1, zero_lt_one, fun a _ => zero_subset.2 <| zero_mem_smul_set h⟩⟩
case intro.intro
𝕜 : Type u_1
𝕝 : Type ?u.204287
E : Type u_2
ι : Sort ?u.204293
κ : ι → Sort ?u.204298
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s : Set E
r : ℝ
hr : 0 < r
h : ∀ (a : 𝕜), r ≤ ‖a‖ → 0 ⊆ a • s
⊢ 0 ∈ s
𝕜 : Type u_1
𝕝 : Type ?u.204287
E : Type u_2
ι : Sort ?u.204293
κ : ι → Sort ?u.204298
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s : Set E
⊢ Absorbs 𝕜 s 0 → 0 ∈ s
rintro ⟨r, hr, h⟩
case intro.intro.intro
𝕜 : Type u_1
𝕝 : Type ?u.204287
E : Type u_2
ι : Sort ?u.204293
κ : ι → Sort ?u.204298
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s : Set E
r : ℝ
hr : 0 < r
h : ∀ (a : 𝕜), r ≤ ‖a‖ → 0 ⊆ a • s
a : 𝕜
ha : r < ‖a‖
⊢ 0 ∈ s
case intro.intro
𝕜 : Type u_1
𝕝 : Type ?u.204287
E : Type u_2
ι : Sort ?u.204293
κ : ι → Sort ?u.204298
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s : Set E
r : ℝ
hr : 0 < r
h : ∀ (a : 𝕜), r ≤ ‖a‖ → 0 ⊆ a • s
⊢ 0 ∈ s
obtain ⟨a, ha⟩ := NormedSpace.exists_lt_norm 𝕜 𝕜 r
case intro.intro.intro
𝕜 : Type u_1
𝕝 : Type ?u.204287
E : Type u_2
ι : Sort ?u.204293
κ : ι → Sort ?u.204298
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s : Set E
r : ℝ
hr : 0 < r
h : ∀ (a : 𝕜), r ≤ ‖a‖ → 0 ⊆ a • s
a : 𝕜
ha : r < ‖a‖
this : 0 ⊆ a • s
⊢ 0 ∈ s
case intro.intro.intro
𝕜 : Type u_1
𝕝 : Type ?u.204287
E : Type u_2
ι : Sort ?u.204293
κ : ι → Sort ?u.204298
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s : Set E
r : ℝ
hr : 0 < r
h : ∀ (a : 𝕜), r ≤ ‖a‖ → 0 ⊆ a • s
a : 𝕜
ha : r < ‖a‖
⊢ 0 ∈ s
have := h _ ha.le
case intro.intro.intro
𝕜 : Type u_1
𝕝 : Type ?u.204287
E : Type u_2
ι : Sort ?u.204293
κ : ι → Sort ?u.204298
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s : Set E
r : ℝ
hr : 0 < r
h : ∀ (a : 𝕜), r ≤ ‖a‖ → 0 ⊆ a • s
a : 𝕜
ha : r < ‖a‖
this : 0 ∈ a • s
⊢ a ≠ 0
case intro.intro.intro
𝕜 : Type u_1
𝕝 : Type ?u.204287
E : Type u_2
ι : Sort ?u.204293
κ : ι → Sort ?u.204298
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s : Set E
r : ℝ
hr : 0 < r
h : ∀ (a : 𝕜), r ≤ ‖a‖ → 0 ⊆ a • s
a : 𝕜
ha : r < ‖a‖
this : 0 ⊆ a • s
⊢ 0 ∈ s
rwa [zero_subset, zero_mem_smul_set_iff] at this
no goals
case intro.intro.intro
𝕜 : Type u_1
𝕝 : Type ?u.204287
E : Type u_2
ι : Sort ?u.204293
κ : ι → Sort ?u.204298
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s : Set E
r : ℝ
hr : 0 < r
h : ∀ (a : 𝕜), r ≤ ‖a‖ → 0 ⊆ a • s
a : 𝕜
ha : r < ‖a‖
this : 0 ∈ a • s
⊢ a ≠ 0
exact norm_ne_zero_iff.1 (hr.trans ha).ne'