Theorem: LocallyLipschitz.restrict (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
f : X → Y
hf : LocallyLipschitz f
s : Set X
⊢ LocallyLipschitz (s.restrict 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
f : X → Y
hf : LocallyLipschitz f
s : Set X
x : ↑s
⊢ ∃ K, ∃ t ∈ 𝓝 x, LipschitzOnWith K (s.restrict 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
f : X → Y
hf : LocallyLipschitz f
s : Set X
x : ↑s
⊢ ∃ K, ∃ t ∈ 𝓝 x, LipschitzOnWith K (s.restrict f) t
Tactic:
rcases hf x with ⟨K, 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✝¹ : MetricSpace Y
inst✝ : MetricSpace Z
f : X → Y
hf : LocallyLipschitz f
s : Set X
x : ↑s
K : ℝ≥0
t : Set X
ht : t ∈ 𝓝 ↑x
hfL : LipschitzOnWith K f t
⊢ ∃ K, ∃ t ∈ 𝓝 x, LipschitzOnWith K (s.restrict 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
f : X → Y
hf : LocallyLipschitz f
s : Set X
x : ↑s
K : ℝ≥0
t : Set X
ht : t ∈ 𝓝 ↑x
hfL : LipschitzOnWith K f t
⊢ ∃ K, ∃ t ∈ 𝓝 x, LipschitzOnWith K (s.restrict f) t
Tactic:
exact ⟨K, toSubset t s, ToSubset.compatible_with_nhds s t ht, LipschitzOnWith.restrict_subtype s t hfL⟩
State after:
no goals