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

State before:
X : Type u_1
Y : Type u_2
Z : Type u_3
inst✝⁶ : MetricSpace X
inst✝⁵ : MetricSpace Y
inst✝⁴ : MetricSpace Z
E : Type u_4
F : Type u_5
f : E → F
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
hf : ContDiff ℝ 1 f
⊢ LocallyLipschitz f
Tactic:
intro x
State after:
X : Type u_1
Y : Type u_2
Z : Type u_3
inst✝⁶ : MetricSpace X
inst✝⁵ : MetricSpace Y
inst✝⁴ : MetricSpace Z
E : Type u_4
F : Type u_5
f : E → F
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
hf : ContDiff ℝ 1 f
x : E
⊢ ∃ K, ∃ t ∈ 𝓝 x, LipschitzOnWith K f t

State before:
X : Type u_1
Y : Type u_2
Z : Type u_3
inst✝⁶ : MetricSpace X
inst✝⁵ : MetricSpace Y
inst✝⁴ : MetricSpace Z
E : Type u_4
F : Type u_5
f : E → F
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
hf : ContDiff ℝ 1 f
x : E
⊢ ∃ K, ∃ t ∈ 𝓝 x, LipschitzOnWith K f t
Tactic:
rcases (ContDiffAt.exists_lipschitzOnWith (ContDiff.contDiffAt hf)) with ⟨K, t, ht, hf⟩
State after:
case intro.intro.intro
X : Type u_1
Y : Type u_2
Z : Type u_3
inst✝⁶ : MetricSpace X
inst✝⁵ : MetricSpace Y
inst✝⁴ : MetricSpace Z
E : Type u_4
F : Type u_5
f : E → F
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
hf✝ : ContDiff ℝ 1 f
x : E
K : ℝ≥0
t : Set E
ht : t ∈ 𝓝 ?m.4791
hf : LipschitzOnWith K f t
⊢ ∃ K, ∃ t ∈ 𝓝 x, LipschitzOnWith K f t

State before:
case intro.intro.intro
X : Type u_1
Y : Type u_2
Z : Type u_3
inst✝⁶ : MetricSpace X
inst✝⁵ : MetricSpace Y
inst✝⁴ : MetricSpace Z
E : Type u_4
F : Type u_5
f : E → F
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
hf✝ : ContDiff ℝ 1 f
x : E
K : ℝ≥0
t : Set E
ht : t ∈ 𝓝 ?m.4791
hf : LipschitzOnWith K f t
⊢ ∃ K, ∃ t ∈ 𝓝 x, LipschitzOnWith K f t
Tactic:
use K, t
State after:
no goals