Theorem: LocallyLipschitz.of_C1_on_open (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
U : Set E
h₁U : IsOpen U
h₂U : Convex ℝ U
hf : ContDiffOn ℝ 1 f U
⊢ LocallyLipschitz (U.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
E : Type u_4
F : Type u_5
f : E → F
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
U : Set E
h₁U : IsOpen U
h₂U : Convex ℝ U
hf : ContDiffOn ℝ 1 f U
x : ↑U
⊢ ∃ K, ∃ t ∈ 𝓝 x, LipschitzOnWith K (U.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
E : Type u_4
F : Type u_5
f : E → F
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
U : Set E
h₁U : IsOpen U
h₂U : Convex ℝ U
hf : ContDiffOn ℝ 1 f U
x : ↑U
⊢ ∃ K, ∃ t ∈ 𝓝 x, LipschitzOnWith K (U.restrict f) t
Tactic:
have : ContDiffWithinAt ℝ 1 f U x := ContDiffOn.contDiffWithinAt hf (Subtype.mem 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
U : Set E
h₁U : IsOpen U
h₂U : Convex ℝ U
hf : ContDiffOn ℝ 1 f U
x : ↑U
this : ContDiffWithinAt ℝ 1 f U ↑x
⊢ ∃ K, ∃ t ∈ 𝓝 x, LipschitzOnWith K (U.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
E : Type u_4
F : Type u_5
f : E → F
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
U : Set E
h₁U : IsOpen U
h₂U : Convex ℝ U
hf : ContDiffOn ℝ 1 f U
x : ↑U
this : ContDiffWithinAt ℝ 1 f U ↑x
⊢ ∃ K, ∃ t ∈ 𝓝 x, LipschitzOnWith K (U.restrict f) t
Tactic:
let h := ContDiffWithinAt.exists_lipschitzOnWith this
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
U : Set E
h₁U : IsOpen U
h₂U : Convex ℝ U
hf : ContDiffOn ℝ 1 f U
x : ↑U
this : ContDiffWithinAt ℝ 1 f U ↑x
h : Convex ℝ U → ∃ K, ∃ t ∈ 𝓝[U] ↑x, LipschitzOnWith K f t := ContDiffWithinAt.exists_lipschitzOnWith this
⊢ ∃ K, ∃ t ∈ 𝓝 x, LipschitzOnWith K (U.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
E : Type u_4
F : Type u_5
f : E → F
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
U : Set E
h₁U : IsOpen U
h₂U : Convex ℝ U
hf : ContDiffOn ℝ 1 f U
x : ↑U
this : ContDiffWithinAt ℝ 1 f U ↑x
h : Convex ℝ U → ∃ K, ∃ t ∈ 𝓝[U] ↑x, LipschitzOnWith K f t := ContDiffWithinAt.exists_lipschitzOnWith this
⊢ ∃ K, ∃ t ∈ 𝓝 x, LipschitzOnWith K (U.restrict f) t
Tactic:
rcases (h h₂U) 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
U : Set E
h₁U : IsOpen U
h₂U : Convex ℝ U
hf✝ : ContDiffOn ℝ 1 f U
x : ↑U
this : ContDiffWithinAt ℝ 1 f U ↑x
h : Convex ℝ U → ∃ K, ∃ t ∈ 𝓝[U] ↑x, LipschitzOnWith K f t := ContDiffWithinAt.exists_lipschitzOnWith this
K : ℝ≥0
t : Set E
ht : t ∈ 𝓝[U] ↑x
hf : LipschitzOnWith K f t
⊢ ∃ K, ∃ t ∈ 𝓝 x, LipschitzOnWith K (U.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
E : Type u_4
F : Type u_5
f : E → F
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
U : Set E
h₁U : IsOpen U
h₂U : Convex ℝ U
hf✝ : ContDiffOn ℝ 1 f U
x : ↑U
this : ContDiffWithinAt ℝ 1 f U ↑x
h : Convex ℝ U → ∃ K, ∃ t ∈ 𝓝[U] ↑x, LipschitzOnWith K f t := ContDiffWithinAt.exists_lipschitzOnWith this
K : ℝ≥0
t : Set E
ht : t ∈ 𝓝[U] ↑x
hf : LipschitzOnWith K f t
⊢ ∃ K, ∃ t ∈ 𝓝 x, LipschitzOnWith K (U.restrict f) t
Tactic:
exact ⟨K, toSubset t U, ToSubset.compatible_with_nhds_within t U h₁U ht, LipschitzOnWith.restrict_subtype U t hf⟩
State after:
no goals