Theorem: LocallyLipschitz.mysmul (Sard/LocallyLipschitz.lean)

State before:
X : Type u_1
Y : Type u_2
Z : Type u_3
inst✝² : MetricSpace X
inst✝¹ : NormedAddCommGroup Y
inst✝ : NormedSpace ℝ Y
f g : X → Y
hf : LocallyLipschitz f
a : ℝ
⊢ LocallyLipschitz fun x => a • f x
Tactic:
intro x
State after:
X : Type u_1
Y : Type u_2
Z : Type u_3
inst✝² : MetricSpace X
inst✝¹ : NormedAddCommGroup Y
inst✝ : NormedSpace ℝ Y
f g : X → Y
hf : LocallyLipschitz f
a : ℝ
x : X
⊢ ∃ K, ∃ t ∈ 𝓝 x, LipschitzOnWith K (fun x => a • f x) t

State before:
X : Type u_1
Y : Type u_2
Z : Type u_3
inst✝² : MetricSpace X
inst✝¹ : NormedAddCommGroup Y
inst✝ : NormedSpace ℝ Y
f g : X → Y
hf : LocallyLipschitz f
a : ℝ
x : X
⊢ ∃ K, ∃ t ∈ 𝓝 x, LipschitzOnWith K (fun x => a • f x) t
Tactic:
rcases hf x with ⟨Kf, t, ht, hfL⟩
State after:
case intro.intro.intro
X : Type u_1
Y : Type u_2
Z : Type u_3
inst✝² : MetricSpace X
inst✝¹ : NormedAddCommGroup Y
inst✝ : NormedSpace ℝ Y
f g : X → Y
hf : LocallyLipschitz f
a : ℝ
x : X
Kf : ℝ≥0
t : Set X
ht : t ∈ 𝓝 x
hfL : LipschitzOnWith Kf f t
⊢ ∃ K, ∃ t ∈ 𝓝 x, LipschitzOnWith K (fun x => a • f x) t

State before:
case intro.intro.intro
X : Type u_1
Y : Type u_2
Z : Type u_3
inst✝² : MetricSpace X
inst✝¹ : NormedAddCommGroup Y
inst✝ : NormedSpace ℝ Y
f g : X → Y
hf : LocallyLipschitz f
a : ℝ
x : X
Kf : ℝ≥0
t : Set X
ht : t ∈ 𝓝 x
hfL : LipschitzOnWith Kf f t
⊢ ∃ K, ∃ t ∈ 𝓝 x, LipschitzOnWith K (fun x => a • f x) t
Tactic:
exact ⟨ENNReal.toNNReal (ENNReal.ofReal ‖a‖) * Kf, t, ht, hfL.smul a⟩
State after:
no goals