internlm/Lean-Github huggingface dataset:
Theorem: interior_zero_iff_open_cover
Proof state before:
case mpr.intro
X : Type
inst✝ : TopologicalSpace X
I : Type
U : I → Set X
hU : ∀ (α : I), IsOpen (U α)
hcover : ↑(⋃ α, U α) = X
s : Set X
h : ∀ (α : I), interior (s ∩ U α) = ∅
V : Set X
hVS : V ⊆ s
hV : IsOpen V
h' : ∀ (α : I), V ∩ U α = ∅
h'' : V = ⋃ α, V ∩ U α
⊢ ⋃ α, V ∩ U α = ∅
Tactic:
simp only [Set.iUnion_eq_empty]
Proof state after:
case mpr.intro
X : Type
inst✝ : TopologicalSpace X
I : Type
U : I → Set X
hU : ∀ (α : I), IsOpen (U α)
hcover : ↑(⋃ α, U α) = X
s : Set X
h : ∀ (α : I), interior (s ∩ U α) = ∅
V : Set X
hVS : V ⊆ s
hV : IsOpen V
h' : ∀ (α : I), V ∩ U α = ∅
h'' : V = ⋃ α, V ∩ U α
⊢ ∀ (i : I), V ∩ U i = ∅
Theorem: interior_zero_iff_open_cover
Proof state before:
case mpr.intro
X : Type
inst✝ : TopologicalSpace X
I : Type
U : I → Set X
hU : ∀ (α : I), IsOpen (U α)
hcover : ↑(⋃ α, U α) = X
s : Set X
h : ∀ (α : I), interior (s ∩ U α) = ∅
V : Set X
hVS : V ⊆ s
hV : IsOpen V
h' : ∀ (α : I), V ∩ U α = ∅
h'' : V = ⋃ α, V ∩ U α
⊢ ∀ (i : I), V ∩ U i = ∅
Tactic:
tauto
Proof state after:
no goals
Theorem: interior_zero_iff_open_cover
Proof state before:
X : Type
inst✝ : TopologicalSpace X
I : Type
U : I → Set X
hU : ∀ (α : I), IsOpen (U α)
hcover : ↑(⋃ α, U α) = X
s : Set X
h : ∀ (α : I), interior (s ∩ U α) = ∅
this : ∀ (V : Set X), V ⊆ s ∧ IsOpen V → V = ∅
⊢ interior s = ∅
Tactic:
sorry
Proof state after:
no goals
Theorem: interior_zero_iff_open_cover
Proof state before:
X : Type
inst✝ : TopologicalSpace X
I : Type
U : I → Set X
hU : ∀ (α : I), IsOpen (U α)
hcover : ↑(⋃ α, U α) = X
s : Set X
h : ∀ (α : I), interior (s ∩ U α) = ∅
V : Set X
hVS : V ⊆ s
hV : IsOpen V
⊢ ∀ (α : I), V ∩ U α = ∅
Tactic:
intro α
Proof state after:
X : Type
inst✝ : TopologicalSpace X
I : Type
U : I → Set X
hU : ∀ (α : I), IsOpen (U α)
hcover : ↑(⋃ α, U α) = X
s : Set X
h : ∀ (α : I), interior (s ∩ U α) = ∅
V : Set X
hVS : V ⊆ s
hV : IsOpen V
α : I
⊢ V ∩ U α = ∅
Theorem: interior_zero_iff_open_cover
Proof state before:
X : Type
inst✝ : TopologicalSpace X
I : Type
U : I → Set X
hU : ∀ (α : I), IsOpen (U α)
hcover : ↑(⋃ α, U α) = X
s : Set X
h : ∀ (α : I), interior (s ∩ U α) = ∅
V : Set X
hVS : V ⊆ s
hV : IsOpen V
α : I
⊢ V ∩ U α = ∅
Tactic:
have h₁ : IsOpen (V ∩ U α) := by exact IsOpen.inter hV (hU α)
Proof state after:
X : Type
inst✝ : TopologicalSpace X
I : Type
U : I → Set X
hU : ∀ (α : I), IsOpen (U α)
hcover : ↑(⋃ α, U α) = X
s : Set X
h : ∀ (α : I), interior (s ∩ U α) = ∅
V : Set X
hVS : V ⊆ s
hV : IsOpen V
α : I
h₁ : IsOpen (V ∩ U α)
⊢ V ∩ U α = ∅
Theorem: interior_zero_iff_open_cover
Proof state before:
X : Type
inst✝ : TopologicalSpace X
I : Type
U : I → Set X
hU : ∀ (α : I), IsOpen (U α)
hcover : ↑(⋃ α, U α) = X
s : Set X
h : ∀ (α : I), interior (s ∩ U α) = ∅
V : Set X
hVS : V ⊆ s
hV : IsOpen V
α : I
h₁ : IsOpen (V ∩ U α)
⊢ V ∩ U α = ∅
Tactic:
have h₂ : V ∩ U α ⊆ s ∩ U α := by exact Set.inter_subset_inter_left (U α) hVS
Proof state after:
X : Type
inst✝ : TopologicalSpace X
I : Type
U : I → Set X
hU : ∀ (α : I), IsOpen (U α)
hcover : ↑(⋃ α, U α) = X
s : Set X
h : ∀ (α : I), interior (s ∩ U α) = ∅
V : Set X
hVS : V ⊆ s
hV : IsOpen V
α : I
h₁ : IsOpen (V ∩ U α)
h₂ : V ∩ U α ⊆ s ∩ U α
⊢ V ∩ U α = ∅
Theorem: interior_zero_iff_open_cover
Proof state before:
X : Type
inst✝ : TopologicalSpace X
I : Type
U : I → Set X
hU : ∀ (α : I), IsOpen (U α)
hcover : ↑(⋃ α, U α) = X
s : Set X
h : ∀ (α : I), interior (s ∩ U α) = ∅
V : Set X
hVS : V ⊆ s
hV : IsOpen V
α : I
h₁ : IsOpen (V ∩ U α)
h₂ : V ∩ U α ⊆ s ∩ U α
⊢ V ∩ U α = ∅
Tactic:
have h₃ : V ∩ U α ⊆ interior (s ∩ U α) := by exact interior_maximal h₂ h₁
Proof state after:
X : Type
inst✝ : TopologicalSpace X
I : Type
U : I → Set X
hU : ∀ (α : I), IsOpen (U α)
hcover : ↑(⋃ α, U α) = X
s : Set X
h : ∀ (α : I), interior (s ∩ U α) = ∅
V : Set X
hVS : V ⊆ s
hV : IsOpen V
α : I
h₁ : IsOpen (V ∩ U α)
h₂ : V ∩ U α ⊆ s ∩ U α
h₃ : V ∩ U α ⊆ interior (s ∩ U α)
⊢ V ∩ U α = ∅
Theorem: interior_zero_iff_open_cover
Proof state before:
X : Type
inst✝ : TopologicalSpace X
I : Type
U : I → Set X
hU : ∀ (α : I), IsOpen (U α)
hcover : ↑(⋃ α, U α) = X
s : Set X
h : ∀ (α : I), interior (s ∩ U α) = ∅
V : Set X
hVS : V ⊆ s
hV : IsOpen V
α : I
h₁ : IsOpen (V ∩ U α)
h₂ : V ∩ U α ⊆ s ∩ U α
h₃ : V ∩ U α ⊆ interior (s ∩ U α)
⊢ V ∩ U α = ∅
Tactic:
exact Set.subset_eq_empty h₃ (h α)
Proof state after:
no goals
Theorem: interior_zero_iff_open_cover
Proof state before:
X : Type
inst✝ : TopologicalSpace X
I : Type
U : I → Set X
hU : ∀ (α : I), IsOpen (U α)
hcover : ↑(⋃ α, U α) = X
s : Set X
h : ∀ (α : I), interior (s ∩ U α) = ∅
V : Set X
hVS : V ⊆ s
hV : IsOpen V
α : I
⊢ IsOpen (V ∩ U α)
Tactic:
exact IsOpen.inter hV (hU α)
Proof state after:
no goals
Theorem: interior_zero_iff_open_cover
Proof state before:
X : Type
inst✝ : TopologicalSpace X
I : Type
U : I → Set X
hU : ∀ (α : I), IsOpen (U α)
hcover : ↑(⋃ α, U α) = X
s : Set X
h : ∀ (α : I), interior (s ∩ U α) = ∅
V : Set X
hVS : V ⊆ s
hV : IsOpen V
α : I
h₁ : IsOpen (V ∩ U α)
⊢ V ∩ U α ⊆ s ∩ U α
Tactic:
exact Set.inter_subset_inter_left (U α) hVS
Proof state after:
no goals
Theorem: interior_zero_iff_open_cover
Proof state before:
X : Type
inst✝ : TopologicalSpace X
I : Type
U : I → Set X
hU : ∀ (α : I), IsOpen (U α)
hcover : ↑(⋃ α, U α) = X
s : Set X
h : ∀ (α : I), interior (s ∩ U α) = ∅
V : Set X
hVS : V ⊆ s
hV : IsOpen V
α : I
h₁ : IsOpen (V ∩ U α)
h₂ : V ∩ U α ⊆ s ∩ U α
⊢ V ∩ U α ⊆ interior (s ∩ U α)
Tactic:
exact interior_maximal h₂ h₁
Proof state after:
no goals
Theorem: interior_zero_iff_open_cover
Proof state before:
X : Type
inst✝ : TopologicalSpace X
I : Type
U : I → Set X
hU : ∀ (α : I), IsOpen (U α)
hcover : ↑(⋃ α, U α) = X
s : Set X
h : ∀ (α : I), interior (s ∩ U α) = ∅
V : Set X
hVS : V ⊆ s
hV : IsOpen V
h' : ∀ (α : I), V ∩ U α = ∅
⊢ V = ⋃ α, V ∩ U α
Tactic:
ext i
Proof state after:
case h
X : Type
inst✝ : TopologicalSpace X
I : Type
U : I → Set X
hU : ∀ (α : I), IsOpen (U α)
hcover : ↑(⋃ α, U α) = X
s : Set X
h : ∀ (α : I), interior (s ∩ U α) = ∅
V : Set X
hVS : V ⊆ s
hV : IsOpen V
h' : ∀ (α : I), V ∩ U α = ∅
i : X
⊢ i ∈ V ↔ i ∈ ⋃ α, V ∩ U α
Theorem: interior_zero_iff_open_cover
Proof state before:
case h
X : Type
inst✝ : TopologicalSpace X
I : Type
U : I → Set X
hU : ∀ (α : I), IsOpen (U α)
hcover : ↑(⋃ α, U α) = X
s : Set X
h : ∀ (α : I), interior (s ∩ U α) = ∅
V : Set X
hVS : V ⊆ s
hV : IsOpen V
h' : ∀ (α : I), V ∩ U α = ∅
i : X
⊢ i ∈ V ↔ i ∈ ⋃ α, V ∩ U α
Tactic:
rw [Set.mem_iUnion]
Proof state after:
case h
X : Type
inst✝ : TopologicalSpace X
I : Type
U : I → Set X
hU : ∀ (α : I), IsOpen (U α)
hcover : ↑(⋃ α, U α) = X
s : Set X
h : ∀ (α : I), interior (s ∩ U α) = ∅
V : Set X
hVS : V ⊆ s
hV : IsOpen V
h' : ∀ (α : I), V ∩ U α = ∅
i : X
⊢ i ∈ V ↔ ∃ i_1, i ∈ V ∩ U i_1
Theorem: interior_zero_iff_open_cover
Proof state before:
case h
X : Type
inst✝ : TopologicalSpace X
I : Type
U : I → Set X
hU : ∀ (α : I), IsOpen (U α)
hcover : ↑(⋃ α, U α) = X
s : Set X
h : ∀ (α : I), interior (s ∩ U α) = ∅
V : Set X
hVS : V ⊆ s
hV : IsOpen V
h' : ∀ (α : I), V ∩ U α = ∅
i : X
⊢ i ∈ V ↔ ∃ i_1, i ∈ V ∩ U i_1
Tactic:
sorry
Proof state after:
no goals
Theorem: LocallyLipschitz.ToSubset.compatible_with_nhds
Proof state before:
X : Type u_1
Y : Type u_2
Z : Type u_3
inst✝² : MetricSpace X
inst✝¹ : MetricSpace Y
inst✝ : MetricSpace Z
s t : Set X
x : ↑s
ht : t ∈ 𝓝 ↑x
⊢ t.toSubset s ∈ 𝓝 x
Tactic:
sorry
Proof state after:
no goals
Theorem: LocallyLipschitz.ToSubset.compatible_with_nhds_within
Proof state before:
X : Type u_1
Y : Type u_2
Z : Type u_3
inst✝² : MetricSpace X
inst✝¹ : MetricSpace Y
inst✝ : MetricSpace Z
t U : Set X
x : ↑U
hU : IsOpen U
ht : t ∈ 𝓝[U] ↑x
this : t ∩ U ∈ 𝓝 ↑x
⊢ t.toSubset U ∈ 𝓝 x
Tactic:
apply ToSubset.compatible_with_nhds
Proof state after:
case ht
X : Type u_1
Y : Type u_2
Z : Type u_3
inst✝² : MetricSpace X
inst✝¹ : MetricSpace Y
inst✝ : MetricSpace Z
t U : Set X
x : ↑U
hU : IsOpen U
ht : t ∈ 𝓝[U] ↑x
this : t ∩ U ∈ 𝓝 ↑x
⊢ t ∈ 𝓝 ↑x
Theorem: LocallyLipschitz.ToSubset.compatible_with_nhds_within
Proof state before:
case ht
X : Type u_1
Y : Type u_2
Z : Type u_3
inst✝² : MetricSpace X
inst✝¹ : MetricSpace Y
inst✝ : MetricSpace Z
t U : Set X
x : ↑U
hU : IsOpen U
ht : t ∈ 𝓝[U] ↑x
this : t ∩ U ∈ 𝓝 ↑x
⊢ t ∈ 𝓝 ↑x
Tactic:
exact Filter.mem_of_superset this (inter_subset_left t U)
Proof state after:
no goals
Theorem: LocallyLipschitz.ToSubset.compatible_with_nhds_within
Proof state before:
X : Type u_1
Y : Type u_2
Z : Type u_3
inst✝² : MetricSpace X
inst✝¹ : MetricSpace Y
inst✝ : MetricSpace Z
t U : Set X
x : ↑U
hU : IsOpen U
ht : t ∈ 𝓝[U] ↑x
⊢ t ∩ U ∈ 𝓝 ↑x
Tactic:
rcases ht with ⟨b, hb, U', hU', htaU⟩
Proof state after:
case intro.intro.intro.intro
X : Type u_1
Y : Type u_2
Z : Type u_3
inst✝² : MetricSpace X
inst✝¹ : MetricSpace Y
inst✝ : MetricSpace Z
t U : Set X
x : ↑U
hU : IsOpen U
b : Set X
hb : b ∈ 𝓝 ↑x
U' : Set X
hU' : U' ∈ Filter.principal U
htaU : t = b ∩ U'
⊢ t ∩ U ∈ 𝓝 ↑x
Theorem: LocallyLipschitz.ToSubset.compatible_with_nhds_within
Proof state before:
case intro.intro.intro.intro
X : Type u_1
Y : Type u_2
Z : Type u_3
inst✝² : MetricSpace X
inst✝¹ : MetricSpace Y
inst✝ : MetricSpace Z
t U : Set X
x : ↑U
hU : IsOpen U
b : Set X
hb : b ∈ 𝓝 ↑x
U' : Set X
hU' : U' ∈ Filter.principal U
htaU : t = b ∩ U'
⊢ t ∩ U ∈ 𝓝 ↑x
Tactic:
rw [mem_nhds_iff] at hb
Proof state after:
case intro.intro.intro.intro
X : Type u_1
Y : Type u_2
Z : Type u_3
inst✝² : MetricSpace X
inst✝¹ : MetricSpace Y
inst✝ : MetricSpace Z
t U : Set X
x : ↑U
hU : IsOpen U
b : Set X
hb : ∃ t ⊆ b, IsOpen t ∧ ↑x ∈ t
U' : Set X
hU' : U' ∈ Filter.principal U
htaU : t = b ∩ U'
⊢ t ∩ U ∈ 𝓝 ↑x
Theorem: LocallyLipschitz.ToSubset.compatible_with_nhds_within
Proof state before:
case intro.intro.intro.intro
X : Type u_1
Y : Type u_2
Z : Type u_3
inst✝² : MetricSpace X
inst✝¹ : MetricSpace Y
inst✝ : MetricSpace Z
t U : Set X
x : ↑U
hU : IsOpen U
b : Set X
hb : ∃ t ⊆ b, IsOpen t ∧ ↑x ∈ t
U' : Set X
hU' : U' ∈ Filter.principal U
htaU : t = b ∩ U'
⊢ t ∩ U ∈ 𝓝 ↑x
Tactic:
rcases hb with ⟨a, ha, haopen, hxa⟩
Proof state after:
case intro.intro.intro.intro.intro.intro.intro
X : Type u_1
Y : Type u_2
Z : Type u_3
inst✝² : MetricSpace X
inst✝¹ : MetricSpace Y
inst✝ : MetricSpace Z
t U : Set X
x : ↑U
hU : IsOpen U
b U' : Set X
hU' : U' ∈ Filter.principal U
htaU : t = b ∩ U'
a : Set X
ha : a ⊆ b
haopen : IsOpen a
hxa : ↑x ∈ a
⊢ t ∩ U ∈ 𝓝 ↑x
Theorem: LocallyLipschitz.ToSubset.compatible_with_nhds_within
Proof state before:
case intro.intro.intro.intro.intro.intro.intro
X : Type u_1
Y : Type u_2
Z : Type u_3
inst✝² : MetricSpace X
inst✝¹ : MetricSpace Y
inst✝ : MetricSpace Z
t U : Set X
x : ↑U
hU : IsOpen U
b U' : Set X
hU' : U' ∈ Filter.principal U
htaU : t = b ∩ U'
a : Set X
ha : a ⊆ b
haopen : IsOpen a
hxa : ↑x ∈ a
⊢ t ∩ U ∈ 𝓝 ↑x
Tactic:
rw [mem_nhds_iff]
Proof state after:
case intro.intro.intro.intro.intro.intro.intro
X : Type u_1
Y : Type u_2
Z : Type u_3
inst✝² : MetricSpace X
inst✝¹ : MetricSpace Y
inst✝ : MetricSpace Z
t U : Set X
x : ↑U
hU : IsOpen U
b U' : Set X
hU' : U' ∈ Filter.principal U
htaU : t = b ∩ U'
a : Set X
ha : a ⊆ b
haopen : IsOpen a
hxa : ↑x ∈ a
⊢ ∃ t_1 ⊆ t ∩ U, IsOpen t_1 ∧ ↑x ∈ t_1
Theorem: LocallyLipschitz.ToSubset.compatible_with_nhds_within
Proof state before:
case intro.intro.intro.intro.intro.intro.intro
X : Type u_1
Y : Type u_2
Z : Type u_3
inst✝² : MetricSpace X
inst✝¹ : MetricSpace Y
inst✝ : MetricSpace Z
t U : Set X
x : ↑U
hU : IsOpen U
b U' : Set X
hU' : U' ∈ Filter.principal U
htaU : t = b ∩ U'
a : Set X
ha : a ⊆ b
haopen : IsOpen a
hxa : ↑x ∈ a
⊢ ∃ t_1 ⊆ t ∩ U, IsOpen t_1 ∧ ↑x ∈ t_1
Tactic:
use a ∩ U
Proof state after:
case h
X : Type u_1
Y : Type u_2
Z : Type u_3
inst✝² : MetricSpace X
inst✝¹ : MetricSpace Y
inst✝ : MetricSpace Z
t U : Set X
x : ↑U
hU : IsOpen U
b U' : Set X
hU' : U' ∈ Filter.principal U
htaU : t = b ∩ U'
a : Set X
ha : a ⊆ b
haopen : IsOpen a
hxa : ↑x ∈ a
⊢ a ∩ U ⊆ t ∩ U ∧ IsOpen (a ∩ U) ∧ ↑x ∈ a ∩ U
Theorem: LocallyLipschitz.ToSubset.compatible_with_nhds_within
Proof state before:
case h
X : Type u_1
Y : Type u_2
Z : Type u_3
inst✝² : MetricSpace X
inst✝¹ : MetricSpace Y
inst✝ : MetricSpace Z
t U : Set X
x : ↑U
hU : IsOpen U
b U' : Set X
hU' : U' ∈ Filter.principal U
htaU : t = b ∩ U'
a : Set X
ha : a ⊆ b
haopen : IsOpen a
hxa : ↑x ∈ a
⊢ a ∩ U ⊆ t ∩ U ∧ IsOpen (a ∩ U) ∧ ↑x ∈ a ∩ U
Tactic:
constructor
Proof state after:
case h.left
X : Type u_1
Y : Type u_2
Z : Type u_3
inst✝² : MetricSpace X
inst✝¹ : MetricSpace Y
inst✝ : MetricSpace Z
t U : Set X
x : ↑U
hU : IsOpen U
b U' : Set X
hU' : U' ∈ Filter.principal U
htaU : t = b ∩ U'
a : Set X
ha : a ⊆ b
haopen : IsOpen a
hxa : ↑x ∈ a
⊢ a ∩ U ⊆ t ∩ U

case h.right
X : Type u_1
Y : Type u_2
Z : Type u_3
inst✝² : MetricSpace X
inst✝¹ : MetricSpace Y
inst✝ : MetricSpace Z
t U : Set X
x : ↑U
hU : IsOpen U
b U' : Set X
hU' : U' ∈ Filter.principal U
htaU : t = b ∩ U'
a : Set X
ha : a ⊆ b
haopen : IsOpen a
hxa : ↑x ∈ a
⊢ IsOpen (a ∩ U) ∧ ↑x ∈ a ∩ U
Theorem: LocallyLipschitz.ToSubset.compatible_with_nhds_within
Proof state before:
case h.left
X : Type u_1
Y : Type u_2
Z : Type u_3
inst✝² : MetricSpace X
inst✝¹ : MetricSpace Y
inst✝ : MetricSpace Z
t U : Set X
x : ↑U
hU : IsOpen U
b U' : Set X
hU' : U' ∈ Filter.principal U
htaU : t = b ∩ U'
a : Set X
ha : a ⊆ b
haopen : IsOpen a
hxa : ↑x ∈ a
⊢ a ∩ U ⊆ t ∩ U
Tactic:
calc a ∩ U
  _ ⊆ b ∩ U := inter_subset_inter_left U ha
  _ = b ∩ (U' ∩ U) := by congr; apply (Set.inter_eq_right.mpr hU').symm
  _ ⊆ (b ∩ U') ∩ U := by rw [inter_assoc]
  _ = t ∩ U := by rw [htaU]
Proof state after:
no goals
Theorem: LocallyLipschitz.ToSubset.compatible_with_nhds_within
Proof state before:
X : Type u_1
Y : Type u_2
Z : Type u_3
inst✝² : MetricSpace X
inst✝¹ : MetricSpace Y
inst✝ : MetricSpace Z
t U : Set X
x : ↑U
hU : IsOpen U
b U' : Set X
hU' : U' ∈ Filter.principal U
htaU : t = b ∩ U'
a : Set X
ha : a ⊆ b
haopen : IsOpen a
hxa : ↑x ∈ a
⊢ b ∩ U = b ∩ (U' ∩ U)
Tactic:
congr
Proof state after:
case e_a
X : Type u_1
Y : Type u_2
Z : Type u_3
inst✝² : MetricSpace X
inst✝¹ : MetricSpace Y
inst✝ : MetricSpace Z
t U : Set X
x : ↑U
hU : IsOpen U
b U' : Set X
hU' : U' ∈ Filter.principal U
htaU : t = b ∩ U'
a : Set X
ha : a ⊆ b
haopen : IsOpen a
hxa : ↑x ∈ a
⊢ U = U' ∩ U
Theorem: LocallyLipschitz.ToSubset.compatible_with_nhds_within
Proof state before:
case e_a
X : Type u_1
Y : Type u_2
Z : Type u_3
inst✝² : MetricSpace X
inst✝¹ : MetricSpace Y
inst✝ : MetricSpace Z
t U : Set X
x : ↑U
hU : IsOpen U
b U' : Set X
hU' : U' ∈ Filter.principal U
htaU : t = b ∩ U'
a : Set X
ha : a ⊆ b
haopen : IsOpen a
hxa : ↑x ∈ a
⊢ U = U' ∩ U
Tactic:
apply (Set.inter_eq_right.mpr hU').symm
Proof state after:
no goals
Theorem: LocallyLipschitz.ToSubset.compatible_with_nhds_within
Proof state before:
X : Type u_1
Y : Type u_2
Z : Type u_3
inst✝² : MetricSpace X
inst✝¹ : MetricSpace Y
inst✝ : MetricSpace Z
t U : Set X
x : ↑U
hU : IsOpen U
b U' : Set X
hU' : U' ∈ Filter.principal U
htaU : t = b ∩ U'
a : Set X
ha : a ⊆ b
haopen : IsOpen a
hxa : ↑x ∈ a
⊢ b ∩ (U' ∩ U) ⊆ b ∩ U' ∩ U
Tactic:
rw [inter_assoc]
Proof state after:
no goals
Theorem: LocallyLipschitz.ToSubset.compatible_with_nhds_within
Proof state before:
X : Type u_1
Y : Type u_2
Z : Type u_3
inst✝² : MetricSpace X
inst✝¹ : MetricSpace Y
inst✝ : MetricSpace Z
t U : Set X
x : ↑U
hU : IsOpen U
b U' : Set X
hU' : U' ∈ Filter.principal U
htaU : t = b ∩ U'
a : Set X
ha : a ⊆ b
haopen : IsOpen a
hxa : ↑x ∈ a
⊢ b ∩ U' ∩ U = t ∩ U
Tactic:
rw [htaU]
Proof state after:
no goals
Theorem: LocallyLipschitz.ToSubset.compatible_with_nhds_within
Proof state before:
case h.right
X : Type u_1
Y : Type u_2
Z : Type u_3
inst✝² : MetricSpace X
inst✝¹ : MetricSpace Y
inst✝ : MetricSpace Z
t U : Set X
x : ↑U
hU : IsOpen U
b U' : Set X
hU' : U' ∈ Filter.principal U
htaU : t = b ∩ U'
a : Set X
ha : a ⊆ b
haopen : IsOpen a
hxa : ↑x ∈ a
⊢ IsOpen (a ∩ U) ∧ ↑x ∈ a ∩ U
Tactic:
exact ⟨IsOpen.inter haopen hU, ⟨hxa, Subtype.mem x⟩⟩
Proof state after:
no goals
Theorem: LocallyLipschitz.restrict
Proof 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
Proof 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
Theorem: LocallyLipschitz.restrict
Proof 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⟩
Proof 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
Theorem: LocallyLipschitz.restrict
Proof 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⟩
Proof state after:
no goals
Theorem: LocallyLipschitz.of_C1
Proof 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
Proof 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
Theorem: LocallyLipschitz.of_C1
Proof 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⟩
Proof 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
Theorem: LocallyLipschitz.of_C1
Proof 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
Proof state after:
no goals
Theorem: LocallyLipschitz.of_C1_on_open
Proof 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
Proof 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
Theorem: LocallyLipschitz.of_C1_on_open
Proof 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)
Proof 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
Theorem: LocallyLipschitz.of_C1_on_open
Proof 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
Proof 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
Theorem: LocallyLipschitz.of_C1_on_open
Proof 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⟩
Proof 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
Theorem: LocallyLipschitz.of_C1_on_open
Proof 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⟩
Proof state after:
no goals