case pos
𝕜 : Type ?u.77419
E : Type u_1
F : Type ?u.77425
inst✝¹ : AddCommGroup E
inst✝ : Module ℝ E
s t : Set E
a✝ : ℝ
hs : Convex ℝ s
h₀ : 0 ∈ s
absorbs : Absorbent ℝ s
a : ℝ
ha : 0 ≤ a
⊢ Convex ℝ {x | gauge s x ≤ a}

case neg
𝕜 : Type ?u.77419
E : Type u_1
F : Type ?u.77425
inst✝¹ : AddCommGroup E
inst✝ : Module ℝ E
s t : Set E
a✝ : ℝ
hs : Convex ℝ s
h₀ : 0 ∈ s
absorbs : Absorbent ℝ s
a : ℝ
ha : ¬0 ≤ a
⊢ Convex ℝ {x | gauge s x ≤ a}
𝕜 : Type ?u.77419
E : Type u_1
F : Type ?u.77425
inst✝¹ : AddCommGroup E
inst✝ : Module ℝ E
s t : Set E
a✝ : ℝ
hs : Convex ℝ s
h₀ : 0 ∈ s
absorbs : Absorbent ℝ s
a : ℝ
⊢ Convex ℝ {x | gauge s x ≤ a}
by_cases ha : 0 ≤ a
case pos
𝕜 : Type ?u.77419
E : Type u_1
F : Type ?u.77425
inst✝¹ : AddCommGroup E
inst✝ : Module ℝ E
s t : Set E
a✝ : ℝ
hs : Convex ℝ s
h₀ : 0 ∈ s
absorbs : Absorbent ℝ s
a : ℝ
ha : 0 ≤ a
⊢ Convex ℝ (⋂ (r : ℝ) (_ : a < r), r • s)
case pos
𝕜 : Type ?u.77419
E : Type u_1
F : Type ?u.77425
inst✝¹ : AddCommGroup E
inst✝ : Module ℝ E
s t : Set E
a✝ : ℝ
hs : Convex ℝ s
h₀ : 0 ∈ s
absorbs : Absorbent ℝ s
a : ℝ
ha : 0 ≤ a
⊢ Convex ℝ {x | gauge s x ≤ a}
rw [gauge_le_eq hs h₀ absorbs ha]
no goals
case pos
𝕜 : Type ?u.77419
E : Type u_1
F : Type ?u.77425
inst✝¹ : AddCommGroup E
inst✝ : Module ℝ E
s t : Set E
a✝ : ℝ
hs : Convex ℝ s
h₀ : 0 ∈ s
absorbs : Absorbent ℝ s
a : ℝ
ha : 0 ≤ a
⊢ Convex ℝ (⋂ (r : ℝ) (_ : a < r), r • s)
exact convex_iInter fun i => convex_iInter fun _ => hs.smul _
case h.e'_6
𝕜 : Type ?u.77419
E : Type u_1
F : Type ?u.77425
inst✝¹ : AddCommGroup E
inst✝ : Module ℝ E
s t : Set E
a✝ : ℝ
hs : Convex ℝ s
h₀ : 0 ∈ s
absorbs : Absorbent ℝ s
a : ℝ
ha : ¬0 ≤ a
⊢ {x | gauge s x ≤ a} = ∅
case neg
𝕜 : Type ?u.77419
E : Type u_1
F : Type ?u.77425
inst✝¹ : AddCommGroup E
inst✝ : Module ℝ E
s t : Set E
a✝ : ℝ
hs : Convex ℝ s
h₀ : 0 ∈ s
absorbs : Absorbent ℝ s
a : ℝ
ha : ¬0 ≤ a
⊢ Convex ℝ {x | gauge s x ≤ a}
convert convex_empty (𝕜 := ℝ) (E := E)
no goals
case h.e'_6
𝕜 : Type ?u.77419
E : Type u_1
F : Type ?u.77425
inst✝¹ : AddCommGroup E
inst✝ : Module ℝ E
s t : Set E
a✝ : ℝ
hs : Convex ℝ s
h₀ : 0 ∈ s
absorbs : Absorbent ℝ s
a : ℝ
ha : ¬0 ≤ a
⊢ {x | gauge s x ≤ a} = ∅
exact eq_empty_iff_forall_not_mem.2 fun x hx => ha <| (gauge_nonneg _).trans hx