𝕜 : Type ?u.71418
E : Type u_1
F : Type ?u.71424
inst✝¹ : AddCommGroup E
inst✝ : Module ℝ E
s t : Set E
a : ℝ
hs : Convex ℝ s
h₀ : 0 ∈ s
absorbs : Absorbent ℝ s
⊢ (⋃ (r : ℝ) (_ : r ∈ Ioo 0 1), r • s) ⊆ s
𝕜 : Type ?u.71418
E : Type u_1
F : Type ?u.71424
inst✝¹ : AddCommGroup E
inst✝ : Module ℝ E
s t : Set E
a : ℝ
hs : Convex ℝ s
h₀ : 0 ∈ s
absorbs : Absorbent ℝ s
⊢ {x | gauge s x < 1} ⊆ s
rw [gauge_lt_eq absorbs]
𝕜 : Type ?u.71418
E : Type u_1
F : Type ?u.71424
inst✝¹ : AddCommGroup E
inst✝ : Module ℝ E
s t : Set E
a : ℝ
hs : Convex ℝ s
h₀ : 0 ∈ s
absorbs : Absorbent ℝ s
r : ℝ
hr : r ∈ Ioo 0 1
x✝ : E
⊢ x✝ ∈ r • s → x✝ ∈ s
𝕜 : Type ?u.71418
E : Type u_1
F : Type ?u.71424
inst✝¹ : AddCommGroup E
inst✝ : Module ℝ E
s t : Set E
a : ℝ
hs : Convex ℝ s
h₀ : 0 ∈ s
absorbs : Absorbent ℝ s
⊢ (⋃ (r : ℝ) (_ : r ∈ Ioo 0 1), r • s) ⊆ s
refine' Set.iUnion₂_subset fun r hr _ => _
case intro.intro
𝕜 : Type ?u.71418
E : Type u_1
F : Type ?u.71424
inst✝¹ : AddCommGroup E
inst✝ : Module ℝ E
s t : Set E
a : ℝ
hs : Convex ℝ s
h₀ : 0 ∈ s
absorbs : Absorbent ℝ s
r : ℝ
hr : r ∈ Ioo 0 1
y : E
hy : y ∈ s
⊢ (fun x => r • x) y ∈ s
𝕜 : Type ?u.71418
E : Type u_1
F : Type ?u.71424
inst✝¹ : AddCommGroup E
inst✝ : Module ℝ E
s t : Set E
a : ℝ
hs : Convex ℝ s
h₀ : 0 ∈ s
absorbs : Absorbent ℝ s
r : ℝ
hr : r ∈ Ioo 0 1
x✝ : E
⊢ x✝ ∈ r • s → x✝ ∈ s
rintro ⟨y, hy, rfl⟩
no goals
case intro.intro
𝕜 : Type ?u.71418
E : Type u_1
F : Type ?u.71424
inst✝¹ : AddCommGroup E
inst✝ : Module ℝ E
s t : Set E
a : ℝ
hs : Convex ℝ s
h₀ : 0 ∈ s
absorbs : Absorbent ℝ s
r : ℝ
hr : r ∈ Ioo 0 1
y : E
hy : y ∈ s
⊢ (fun x => r • x) y ∈ s
exact hs.smul_mem_of_zero_mem h₀ hy (Ioo_subset_Icc_self hr)