internlm/Lean-Github huggingface dataset:
Theorem: main
Proof state before:
case intro.intro.intro
ι : Type u_1
l : Filter ι
U : Set ℂ
z₀✝ : ℂ
inst✝ : good_domain U
z₀ : ℂ
hz₀ : z₀ ∈ U
hU : IsOpen U
hU' : IsPreconnected U
h1 : ContinuousOn (obs z₀) (𝓙 U)
f : 𝓒 U
hf : f ∈ 𝓙 U
hfg : ∀ y ∈ 𝓙 U, obs z₀ y ≤ obs z₀ f
h7 : ¬∃ w, EqOn f (fun x => w) U
h5 : f ∈ 𝓘 U
⊢ f '' U = ball 0 1
Tactic:
have h10 : f '' U ⊆ ball 0 1 := by
  have := ((hf.1.1.analyticOn hU).is_constant_or_isOpen hU').resolve_left h7 U subset_rfl hU
  simpa [interior_closedBall] using this.subset_interior_iff.2 (mapsTo'.1 hf.1.2)
Proof state after:
case intro.intro.intro
ι : Type u_1
l : Filter ι
U : Set ℂ
z₀✝ : ℂ
inst✝ : good_domain U
z₀ : ℂ
hz₀ : z₀ ∈ U
hU : IsOpen U
hU' : IsPreconnected U
h1 : ContinuousOn (obs z₀) (𝓙 U)
f : 𝓒 U
hf : f ∈ 𝓙 U
hfg : ∀ y ∈ 𝓙 U, obs z₀ y ≤ obs z₀ f
h7 : ¬∃ w, EqOn f (fun x => w) U
h5 : f ∈ 𝓘 U
h10 : f '' U ⊆ ball 0 1
⊢ f '' U = ball 0 1
Theorem: main
Proof state before:
case intro.intro.intro
ι : Type u_1
l : Filter ι
U : Set ℂ
z₀✝ : ℂ
inst✝ : good_domain U
z₀ : ℂ
hz₀ : z₀ ∈ U
hU : IsOpen U
hU' : IsPreconnected U
h1 : ContinuousOn (obs z₀) (𝓙 U)
f : 𝓒 U
hf : f ∈ 𝓙 U
hfg : ∀ y ∈ 𝓙 U, obs z₀ y ≤ obs z₀ f
h7 : ¬∃ w, EqOn f (fun x => w) U
h5 : f ∈ 𝓘 U
h10 : f '' U ⊆ ball 0 1
⊢ f '' U = ball 0 1
Tactic:
refine (subset_iff_ssubset_or_eq.1 h10).resolve_left ?_
Proof state after:
case intro.intro.intro
ι : Type u_1
l : Filter ι
U : Set ℂ
z₀✝ : ℂ
inst✝ : good_domain U
z₀ : ℂ
hz₀ : z₀ ∈ U
hU : IsOpen U
hU' : IsPreconnected U
h1 : ContinuousOn (obs z₀) (𝓙 U)
f : 𝓒 U
hf : f ∈ 𝓙 U
hfg : ∀ y ∈ 𝓙 U, obs z₀ y ≤ obs z₀ f
h7 : ¬∃ w, EqOn f (fun x => w) U
h5 : f ∈ 𝓘 U
h10 : f '' U ⊆ ball 0 1
⊢ ¬f '' U ⊂ ball 0 1
Theorem: main
Proof state before:
case intro.intro.intro
ι : Type u_1
l : Filter ι
U : Set ℂ
z₀✝ : ℂ
inst✝ : good_domain U
z₀ : ℂ
hz₀ : z₀ ∈ U
hU : IsOpen U
hU' : IsPreconnected U
h1 : ContinuousOn (obs z₀) (𝓙 U)
f : 𝓒 U
hf : f ∈ 𝓙 U
hfg : ∀ y ∈ 𝓙 U, obs z₀ y ≤ obs z₀ f
h7 : ¬∃ w, EqOn f (fun x => w) U
h5 : f ∈ 𝓘 U
h10 : f '' U ⊆ ball 0 1
⊢ ¬f '' U ⊂ ball 0 1
Tactic:
contrapose! hfg
Proof state after:
case intro.intro.intro
ι : Type u_1
l : Filter ι
U : Set ℂ
z₀✝ : ℂ
inst✝ : good_domain U
z₀ : ℂ
hz₀ : z₀ ∈ U
hU : IsOpen U
hU' : IsPreconnected U
h1 : ContinuousOn (obs z₀) (𝓙 U)
f : 𝓒 U
hf : f ∈ 𝓙 U
h7 : ¬∃ w, EqOn f (fun x => w) U
h5 : f ∈ 𝓘 U
h10 : f '' U ⊆ ball 0 1
hfg : f '' U ⊂ ball 0 1
⊢ ∃ y ∈ 𝓙 U, obs z₀ f < obs z₀ y
Theorem: main
Proof state before:
case intro.intro.intro
ι : Type u_1
l : Filter ι
U : Set ℂ
z₀✝ : ℂ
inst✝ : good_domain U
z₀ : ℂ
hz₀ : z₀ ∈ U
hU : IsOpen U
hU' : IsPreconnected U
h1 : ContinuousOn (obs z₀) (𝓙 U)
f : 𝓒 U
hf : f ∈ 𝓙 U
h7 : ¬∃ w, EqOn f (fun x => w) U
h5 : f ∈ 𝓘 U
h10 : f '' U ⊆ ball 0 1
hfg : f '' U ⊂ ball 0 1
⊢ ∃ y ∈ 𝓙 U, obs z₀ f < obs z₀ y
Tactic:
obtain ⟨g, hg⟩ := step_2 U hz₀ ⟨f, hf.1.1, h5.2, mapsTo'.2 h10⟩ hfg
Proof state after:
case intro.intro.intro.intro
ι : Type u_1
l : Filter ι
U : Set ℂ
z₀✝ : ℂ
inst✝ : good_domain U
z₀ : ℂ
hz₀ : z₀ ∈ U
hU : IsOpen U
hU' : IsPreconnected U
h1 : ContinuousOn (obs z₀) (𝓙 U)
f : 𝓒 U
hf : f ∈ 𝓙 U
h7 : ¬∃ w, EqOn f (fun x => w) U
h5 : f ∈ 𝓘 U
h10 : f '' U ⊆ ball 0 1
hfg : f '' U ⊂ ball 0 1
g : embedding U 𝔻
hg : ‖deriv { to_fun := f, is_diff := ⋯, is_inj := ⋯, maps_to := ⋯ }.to_fun z₀‖ < ‖deriv g.to_fun z₀‖
⊢ ∃ y ∈ 𝓙 U, obs z₀ f < obs z₀ y
Theorem: main
Proof state before:
case intro.intro.intro.intro
ι : Type u_1
l : Filter ι
U : Set ℂ
z₀✝ : ℂ
inst✝ : good_domain U
z₀ : ℂ
hz₀ : z₀ ∈ U
hU : IsOpen U
hU' : IsPreconnected U
h1 : ContinuousOn (obs z₀) (𝓙 U)
f : 𝓒 U
hf : f ∈ 𝓙 U
h7 : ¬∃ w, EqOn f (fun x => w) U
h5 : f ∈ 𝓘 U
h10 : f '' U ⊆ ball 0 1
hfg : f '' U ⊂ ball 0 1
g : embedding U 𝔻
hg : ‖deriv { to_fun := f, is_diff := ⋯, is_inj := ⋯, maps_to := ⋯ }.to_fun z₀‖ < ‖deriv g.to_fun z₀‖
⊢ ∃ y ∈ 𝓙 U, obs z₀ f < obs z₀ y
Tactic:
exact ⟨g.to_fun, 𝓘_subset_𝓙 ⟨⟨g.is_diff, g.maps_to.mono_right ball_subset_closedBall⟩, g.is_inj⟩, hg⟩
Proof state after:
no goals
Theorem: main
Proof state before:
ι : Type u_1
l : Filter ι
U : Set ℂ
z₀✝ : ℂ
inst✝ : good_domain U
z₀ : ℂ
hz₀ : z₀ ∈ U
hU : IsOpen U
hU' : IsPreconnected U
h1 : ContinuousOn (obs z₀) (𝓙 U)
f : 𝓒 U
hf : f ∈ 𝓙 U
hfg : ∀ y ∈ 𝓙 U, obs z₀ y ≤ obs z₀ f
⊢ ¬∃ w, EqOn f (fun x => w) U
Tactic:
obtain ⟨g, hg⟩ : (𝓘 U).Nonempty := 𝓘_nonempty
Proof state after:
case intro
ι : Type u_1
l : Filter ι
U : Set ℂ
z₀✝ : ℂ
inst✝ : good_domain U
z₀ : ℂ
hz₀ : z₀ ∈ U
hU : IsOpen U
hU' : IsPreconnected U
h1 : ContinuousOn (obs z₀) (𝓙 U)
f : 𝓒 U
hf : f ∈ 𝓙 U
hfg : ∀ y ∈ 𝓙 U, obs z₀ y ≤ obs z₀ f
g : 𝓒 U
hg : g ∈ 𝓘 U
⊢ ¬∃ w, EqOn f (fun x => w) U
Theorem: main
Proof state before:
case intro
ι : Type u_1
l : Filter ι
U : Set ℂ
z₀✝ : ℂ
inst✝ : good_domain U
z₀ : ℂ
hz₀ : z₀ ∈ U
hU : IsOpen U
hU' : IsPreconnected U
h1 : ContinuousOn (obs z₀) (𝓙 U)
f : 𝓒 U
hf : f ∈ 𝓙 U
hfg : ∀ y ∈ 𝓙 U, obs z₀ y ≤ obs z₀ f
g : 𝓒 U
hg : g ∈ 𝓘 U
⊢ ¬∃ w, EqOn f (fun x => w) U
Tactic:
specialize hfg g (𝓘_subset_𝓙 hg)
Proof state after:
case intro
ι : Type u_1
l : Filter ι
U : Set ℂ
z₀✝ : ℂ
inst✝ : good_domain U
z₀ : ℂ
hz₀ : z₀ ∈ U
hU : IsOpen U
hU' : IsPreconnected U
h1 : ContinuousOn (obs z₀) (𝓙 U)
f : 𝓒 U
hf : f ∈ 𝓙 U
g : 𝓒 U
hg : g ∈ 𝓘 U
hfg : obs z₀ g ≤ obs z₀ f
⊢ ¬∃ w, EqOn f (fun x => w) U
Theorem: main
Proof state before:
case intro
ι : Type u_1
l : Filter ι
U : Set ℂ
z₀✝ : ℂ
inst✝ : good_domain U
z₀ : ℂ
hz₀ : z₀ ∈ U
hU : IsOpen U
hU' : IsPreconnected U
h1 : ContinuousOn (obs z₀) (𝓙 U)
f : 𝓒 U
hf : f ∈ 𝓙 U
g : 𝓒 U
hg : g ∈ 𝓘 U
hfg : obs z₀ g ≤ obs z₀ f
⊢ ¬∃ w, EqOn f (fun x => w) U
Tactic:
have := norm_pos_iff.1 ((norm_pos_iff.2 (deriv_ne_zero_of_inj hU hg.1.1 hg.2 hz₀)).trans_le hfg)
Proof state after:
case intro
ι : Type u_1
l : Filter ι
U : Set ℂ
z₀✝ : ℂ
inst✝ : good_domain U
z₀ : ℂ
hz₀ : z₀ ∈ U
hU : IsOpen U
hU' : IsPreconnected U
h1 : ContinuousOn (obs z₀) (𝓙 U)
f : 𝓒 U
hf : f ∈ 𝓙 U
g : 𝓒 U
hg : g ∈ 𝓘 U
hfg : obs z₀ g ≤ obs z₀ f
this : deriv f z₀ ≠ 0
⊢ ¬∃ w, EqOn f (fun x => w) U
Theorem: main
Proof state before:
case intro
ι : Type u_1
l : Filter ι
U : Set ℂ
z₀✝ : ℂ
inst✝ : good_domain U
z₀ : ℂ
hz₀ : z₀ ∈ U
hU : IsOpen U
hU' : IsPreconnected U
h1 : ContinuousOn (obs z₀) (𝓙 U)
f : 𝓒 U
hf : f ∈ 𝓙 U
g : 𝓒 U
hg : g ∈ 𝓘 U
hfg : obs z₀ g ≤ obs z₀ f
this : deriv f z₀ ≠ 0
⊢ ¬∃ w, EqOn f (fun x => w) U
Tactic:
contrapose! this
Proof state after:
case intro
ι : Type u_1
l : Filter ι
U : Set ℂ
z₀✝ : ℂ
inst✝ : good_domain U
z₀ : ℂ
hz₀ : z₀ ∈ U
hU : IsOpen U
hU' : IsPreconnected U
h1 : ContinuousOn (obs z₀) (𝓙 U)
f : 𝓒 U
hf : f ∈ 𝓙 U
g : 𝓒 U
hg : g ∈ 𝓘 U
hfg : obs z₀ g ≤ obs z₀ f
this : ∃ w, EqOn f (fun x => w) U
⊢ deriv f z₀ = 0
Theorem: main
Proof state before:
case intro
ι : Type u_1
l : Filter ι
U : Set ℂ
z₀✝ : ℂ
inst✝ : good_domain U
z₀ : ℂ
hz₀ : z₀ ∈ U
hU : IsOpen U
hU' : IsPreconnected U
h1 : ContinuousOn (obs z₀) (𝓙 U)
f : 𝓒 U
hf : f ∈ 𝓙 U
g : 𝓒 U
hg : g ∈ 𝓘 U
hfg : obs z₀ g ≤ obs z₀ f
this : ∃ w, EqOn f (fun x => w) U
⊢ deriv f z₀ = 0
Tactic:
obtain ⟨w, hw : EqOn f (λ _ => w) U⟩ := this
Proof state after:
case intro.intro
ι : Type u_1
l : Filter ι
U : Set ℂ
z₀✝ : ℂ
inst✝ : good_domain U
z₀ : ℂ
hz₀ : z₀ ∈ U
hU : IsOpen U
hU' : IsPreconnected U
h1 : ContinuousOn (obs z₀) (𝓙 U)
f : 𝓒 U
hf : f ∈ 𝓙 U
g : 𝓒 U
hg : g ∈ 𝓘 U
hfg : obs z₀ g ≤ obs z₀ f
w : ℂ
hw : EqOn f (fun x => w) U
⊢ deriv f z₀ = 0
Theorem: main
Proof state before:
case intro.intro
ι : Type u_1
l : Filter ι
U : Set ℂ
z₀✝ : ℂ
inst✝ : good_domain U
z₀ : ℂ
hz₀ : z₀ ∈ U
hU : IsOpen U
hU' : IsPreconnected U
h1 : ContinuousOn (obs z₀) (𝓙 U)
f : 𝓒 U
hf : f ∈ 𝓙 U
g : 𝓒 U
hg : g ∈ 𝓘 U
hfg : obs z₀ g ≤ obs z₀ f
w : ℂ
hw : EqOn f (fun x => w) U
⊢ deriv f z₀ = 0
Tactic:
simpa only [deriv_const'] using (hw.eventuallyEq_of_mem (hU.mem_nhds hz₀)).deriv_eq
Proof state after:
no goals
Theorem: main
Proof state before:
ι : Type u_1
l : Filter ι
U : Set ℂ
z₀✝ : ℂ
inst✝ : good_domain U
z₀ : ℂ
hz₀ : z₀ ∈ U
hU : IsOpen U
hU' : IsPreconnected U
h1 : ContinuousOn (obs z₀) (𝓙 U)
f : 𝓒 U
hf : f ∈ 𝓙 U
hfg : ∀ y ∈ 𝓙 U, obs z₀ y ≤ obs z₀ f
h7 : ¬∃ w, EqOn f (fun x => w) U
h5 : f ∈ 𝓘 U
⊢ f '' U ⊆ ball 0 1
Tactic:
have := ((hf.1.1.analyticOn hU).is_constant_or_isOpen hU').resolve_left h7 U subset_rfl hU
Proof state after:
ι : Type u_1
l : Filter ι
U : Set ℂ
z₀✝ : ℂ
inst✝ : good_domain U
z₀ : ℂ
hz₀ : z₀ ∈ U
hU : IsOpen U
hU' : IsPreconnected U
h1 : ContinuousOn (obs z₀) (𝓙 U)
f : 𝓒 U
hf : f ∈ 𝓙 U
hfg : ∀ y ∈ 𝓙 U, obs z₀ y ≤ obs z₀ f
h7 : ¬∃ w, EqOn f (fun x => w) U
h5 : f ∈ 𝓘 U
this : IsOpen (f '' U)
⊢ f '' U ⊆ ball 0 1
Theorem: main
Proof state before:
ι : Type u_1
l : Filter ι
U : Set ℂ
z₀✝ : ℂ
inst✝ : good_domain U
z₀ : ℂ
hz₀ : z₀ ∈ U
hU : IsOpen U
hU' : IsPreconnected U
h1 : ContinuousOn (obs z₀) (𝓙 U)
f : 𝓒 U
hf : f ∈ 𝓙 U
hfg : ∀ y ∈ 𝓙 U, obs z₀ y ≤ obs z₀ f
h7 : ¬∃ w, EqOn f (fun x => w) U
h5 : f ∈ 𝓘 U
this : IsOpen (f '' U)
⊢ f '' U ⊆ ball 0 1
Tactic:
simpa [interior_closedBall] using this.subset_interior_iff.2 (mapsTo'.1 hf.1.2)
Proof state after:
no goals
Theorem: RMT
Proof state before:
ι : Type u_1
l : Filter ι
U : Set ℂ
z₀ : ℂ
h1 : IsOpen U
h2 : IsConnected U
h3 : U ≠ univ
h4 : has_primitives U
⊢ ∃ f, DifferentiableOn ℂ f U ∧ InjOn f U ∧ f '' U = ball 0 1
Tactic:
have : good_domain U := ⟨h1, h2.1, h2.2, h3, (h4.has_logs h1 h2.isPreconnected).has_sqrt⟩
Proof state after:
ι : Type u_1
l : Filter ι
U : Set ℂ
z₀ : ℂ
h1 : IsOpen U
h2 : IsConnected U
h3 : U ≠ univ
h4 : has_primitives U
this : good_domain U
⊢ ∃ f, DifferentiableOn ℂ f U ∧ InjOn f U ∧ f '' U = ball 0 1
Theorem: RMT
Proof state before:
ι : Type u_1
l : Filter ι
U : Set ℂ
z₀ : ℂ
h1 : IsOpen U
h2 : IsConnected U
h3 : U ≠ univ
h4 : has_primitives U
this : good_domain U
⊢ ∃ f, DifferentiableOn ℂ f U ∧ InjOn f U ∧ f '' U = ball 0 1
Tactic:
obtain ⟨f, hf : f ∈ 𝓘 U, hfU⟩ := main (U := U)
Proof state after:
case intro.intro
ι : Type u_1
l : Filter ι
U : Set ℂ
z₀ : ℂ
h1 : IsOpen U
h2 : IsConnected U
h3 : U ≠ univ
h4 : has_primitives U
this : good_domain U
f : 𝓒 U
hf : f ∈ 𝓘 U
hfU : f '' U = ball 0 1
⊢ ∃ f, DifferentiableOn ℂ f U ∧ InjOn f U ∧ f '' U = ball 0 1
Theorem: RMT
Proof state before:
case intro.intro
ι : Type u_1
l : Filter ι
U : Set ℂ
z₀ : ℂ
h1 : IsOpen U
h2 : IsConnected U
h3 : U ≠ univ
h4 : has_primitives U
this : good_domain U
f : 𝓒 U
hf : f ∈ 𝓘 U
hfU : f '' U = ball 0 1
⊢ ∃ f, DifferentiableOn ℂ f U ∧ InjOn f U ∧ f '' U = ball 0 1
Tactic:
exact ⟨f, hf.1.1, hf.2, hfU⟩
Proof state after:
no goals
Theorem: UniformSpace.mem_thickening
Proof state before:
ι : Type u_1
α : Type u_2
β : Type u_3
a : α
s t : Set α
x u v : Set (α × α)
⊢ a ∈ thickening u s ↔ ∃ x ∈ s, (x, a) ∈ u
Tactic:
simp only [thickening, ball, mem_iUnion, mem_preimage, exists_prop]
Proof state after:
no goals
Theorem: UniformSpace.thickening_singleton
Proof state before:
ι : Type u_1
α : Type u_2
β : Type u_3
a : α
s t : Set α
x u v : Set (α × α)
⊢ thickening u {a} = ball a u
Tactic:
simp only [thickening, mem_singleton_iff, iUnion_iUnion_eq_left]
Proof state after:
no goals
Theorem: UniformSpace.monotone_thickening
Proof state before:
ι : Type u_1
α : Type u_2
β : Type u_3
a : α
s t : Set α
x u v : Set (α × α)
⊢ Monotone fun x => thickening x s
Tactic:
intro u v huv
Proof state after:
ι : Type u_1
α : Type u_2
β : Type u_3
a : α
s t : Set α
x u✝ v✝ u v : Set (α × α)
huv : u ≤ v
⊢ (fun x => thickening x s) u ≤ (fun x => thickening x s) v
Theorem: UniformSpace.monotone_thickening
Proof state before:
ι : Type u_1
α : Type u_2
β : Type u_3
a : α
s t : Set α
x u✝ v✝ u v : Set (α × α)
huv : u ≤ v
⊢ (fun x => thickening x s) u ≤ (fun x => thickening x s) v
Tactic:
apply iUnion₂_mono
Proof state after:
case h
ι : Type u_1
α : Type u_2
β : Type u_3
a : α
s t : Set α
x u✝ v✝ u v : Set (α × α)
huv : u ≤ v
⊢ ∀ i ∈ s, ball i u ⊆ ball i v
Theorem: UniformSpace.monotone_thickening
Proof state before:
case h
ι : Type u_1
α : Type u_2
β : Type u_3
a : α
s t : Set α
x u✝ v✝ u v : Set (α × α)
huv : u ≤ v
⊢ ∀ i ∈ s, ball i u ⊆ ball i v
Tactic:
simp only [ball, le_eq_subset] at huv ⊢
Proof state after:
case h
ι : Type u_1
α : Type u_2
β : Type u_3
a : α
s t : Set α
x u✝ v✝ u v : Set (α × α)
huv : u ⊆ v
⊢ ∀ i ∈ s, Prod.mk i ⁻¹' u ⊆ Prod.mk i ⁻¹' v
Theorem: UniformSpace.monotone_thickening
Proof state before:
case h
ι : Type u_1
α : Type u_2
β : Type u_3
a : α
s t : Set α
x u✝ v✝ u v : Set (α × α)
huv : u ⊆ v
⊢ ∀ i ∈ s, Prod.mk i ⁻¹' u ⊆ Prod.mk i ⁻¹' v
Tactic:
exact λ _ _ => preimage_mono huv
Proof state after:
no goals
Theorem: UniformSpace.thickening_comp
Proof state before:
ι : Type u_1
α : Type u_2
β : Type u_3
a : α
s t : Set α
x u v : Set (α × α)
⊢ thickening v (thickening u s) = thickening (u ○ v) s
Tactic:
ext
Proof state after:
case h
ι : Type u_1
α : Type u_2
β : Type u_3
a : α
s t : Set α
x u v : Set (α × α)
x✝ : α
⊢ x✝ ∈ thickening v (thickening u s) ↔ x✝ ∈ thickening (u ○ v) s
Theorem: UniformSpace.thickening_comp
Proof state before:
case h
ι : Type u_1
α : Type u_2
β : Type u_3
a : α
s t : Set α
x u v : Set (α × α)
x✝ : α
⊢ x✝ ∈ thickening v (thickening u s) ↔ x✝ ∈ thickening (u ○ v) s
Tactic:
simp [thickening, ball]
Proof state after:
no goals
Theorem: UniformSpace.disjoint_ball_iff
Proof state before:
ι : Type u_1
α : Type u_2
β : Type u_3
a : α
s t : Set α
x u v : Set (α × α)
⊢ Disjoint (ball a u) t ↔ ∀ b ∈ t, (a, b) ∉ u
Tactic:
rw [← compl_compl (ball a u), disjoint_compl_left_iff_subset]
Proof state after:
ι : Type u_1
α : Type u_2
β : Type u_3
a : α
s t : Set α
x u v : Set (α × α)
⊢ t ⊆ (ball a u)ᶜ ↔ ∀ b ∈ t, (a, b) ∉ u
Theorem: UniformSpace.disjoint_ball_iff
Proof state before:
ι : Type u_1
α : Type u_2
β : Type u_3
a : α
s t : Set α
x u v : Set (α × α)
⊢ t ⊆ (ball a u)ᶜ ↔ ∀ b ∈ t, (a, b) ∉ u
Tactic:
rfl
Proof state after:
no goals
Theorem: UniformSpace.thickening_inter_eq_empty
Proof state before:
ι : Type u_1
α : Type u_2
β : Type u_3
a : α
s t : Set α
x u v : Set (α × α)
⊢ thickening u s ∩ t = ∅ ↔ ∀ a ∈ s, ∀ b ∈ t, (a, b) ∉ u
Tactic:
simp [thickening, ← disjoint_iff_inter_eq_empty, disjoint_ball_iff]
Proof state after:
no goals
Theorem: UniformSpace.thickening_inter_eq_empty_comm
Proof state before:
ι : Type u_1
α : Type u_2
β : Type u_3
a : α
s t : Set α
x u v : Set (α × α)
hu : SymmetricRel u
⊢ thickening u s ∩ t = ∅ ↔ s ∩ thickening u t = ∅
Tactic:
simp [thickening_inter_eq_empty, inter_comm s]
Proof state after:
ι : Type u_1
α : Type u_2
β : Type u_3
a : α
s t : Set α
x u v : Set (α × α)
hu : SymmetricRel u
⊢ (∀ a ∈ s, ∀ b ∈ t, (a, b) ∉ u) ↔ ∀ a ∈ t, ∀ b ∈ s, (a, b) ∉ u
Theorem: UniformSpace.thickening_inter_eq_empty_comm
Proof state before:
ι : Type u_1
α : Type u_2
β : Type u_3
a : α
s t : Set α
x u v : Set (α × α)
hu : SymmetricRel u
⊢ (∀ a ∈ s, ∀ b ∈ t, (a, b) ∉ u) ↔ ∀ a ∈ t, ∀ b ∈ s, (a, b) ∉ u
Tactic:
apply Iff.intro
Proof state after:
case mp
ι : Type u_1
α : Type u_2
β : Type u_3
a : α
s t : Set α
x u v : Set (α × α)
hu : SymmetricRel u
⊢ (∀ a ∈ s, ∀ b ∈ t, (a, b) ∉ u) → ∀ a ∈ t, ∀ b ∈ s, (a, b) ∉ u

case mpr
ι : Type u_1
α : Type u_2
β : Type u_3
a : α
s t : Set α
x u v : Set (α × α)
hu : SymmetricRel u
⊢ (∀ a ∈ t, ∀ b ∈ s, (a, b) ∉ u) → ∀ a ∈ s, ∀ b ∈ t, (a, b) ∉ u
Theorem: UniformSpace.thickening_inter_eq_empty_comm
Proof state before:
case mp
ι : Type u_1
α : Type u_2
β : Type u_3
a : α
s t : Set α
x u v : Set (α × α)
hu : SymmetricRel u
⊢ (∀ a ∈ s, ∀ b ∈ t, (a, b) ∉ u) → ∀ a ∈ t, ∀ b ∈ s, (a, b) ∉ u

case mpr
ι : Type u_1
α : Type u_2
β : Type u_3
a : α
s t : Set α
x u v : Set (α × α)
hu : SymmetricRel u
⊢ (∀ a ∈ t, ∀ b ∈ s, (a, b) ∉ u) → ∀ a ∈ s, ∀ b ∈ t, (a, b) ∉ u
Tactic:
repeat exact λ h a ha b hb hab => h b hb a ha (hu.mk_mem_comm.mp hab)
Proof state after:
no goals
Theorem: UniformSpace.thickening_inter_eq_empty_comm
Proof state before:
case mpr
ι : Type u_1
α : Type u_2
β : Type u_3
a : α
s t : Set α
x u v : Set (α × α)
hu : SymmetricRel u
⊢ (∀ a ∈ t, ∀ b ∈ s, (a, b) ∉ u) → ∀ a ∈ s, ∀ b ∈ t, (a, b) ∉ u
Tactic:
exact λ h a ha b hb hab => h b hb a ha (hu.mk_mem_comm.mp hab)
Proof state after:
no goals
Theorem: UniformSpace.thickening_inter_thickening_eq_empty_of_comp
Proof state before:
ι : Type u_1
α : Type u_2
β : Type u_3
a : α
s t : Set α
x u v : Set (α × α)
hv : SymmetricRel v
hvu : v ○ v ⊆ u
hST : thickening u s ∩ t = ∅
⊢ thickening v s ∩ thickening v t = ∅
Tactic:
simp only [←thickening_inter_eq_empty_comm hv, thickening_comp]
Proof state after:
ι : Type u_1
α : Type u_2
β : Type u_3
a : α
s t : Set α
x u v : Set (α × α)
hv : SymmetricRel v
hvu : v ○ v ⊆ u
hST : thickening u s ∩ t = ∅
⊢ thickening (v ○ v) s ∩ t = ∅
Theorem: UniformSpace.thickening_inter_thickening_eq_empty_of_comp
Proof state before:
ι : Type u_1
α : Type u_2
β : Type u_3
a : α
s t : Set α
x u v : Set (α × α)
hv : SymmetricRel v
hvu : v ○ v ⊆ u
hST : thickening u s ∩ t = ∅
⊢ thickening (v ○ v) s ∩ t = ∅
Tactic:
exact subset_eq_empty (inter_subset_inter_left _ (monotone_thickening hvu)) hST
Proof state after:
no goals
Theorem: UniformSpace.uniform_nhds_set_singleton
Proof state before:
ι : Type u_1
α : Type u_2
β : Type u_3
a✝ : α
s t : Set α
x u v : Set (α × α)
inst✝ : UniformSpace α
a : α
⊢ 𝓝ᵘ {a} = 𝓝 a
Tactic:
simp only [uniform_nhds_set, thickening_singleton, nhds_eq_uniformity]
Proof state after:
no goals
Theorem: UniformSpace.mem_uniform_nhds_set_iff
Proof state before:
ι : Type u_1
α : Type u_2
β : Type u_3
a : α
s t : Set α
x u v : Set (α × α)
inst✝ : UniformSpace α
⊢ s ∈ 𝓝ᵘ t ↔ ∃ u ∈ 𝓤 α, thickening u t ⊆ s
Tactic:
simp [uniform_nhds_set, mem_lift'_sets]
Proof state after:
no goals
Theorem: UniformSpace.nhds_le_uniform_nhds_set
Proof state before:
ι : Type u_1
α : Type u_2
β : Type u_3
a : α
s✝ t : Set α
x u v : Set (α × α)
inst✝ : UniformSpace α
s : Set α
ha : a ∈ s
⊢ 𝓝 a ≤ 𝓝ᵘ s
Tactic:
simpa [← uniform_nhds_set_singleton] using uniform_nhds_set_mono (singleton_subset_iff.mpr ha)
Proof state after:
no goals
Theorem: UniformSpace.nhds_set_le_uniform_nhds_set
Proof state before:
ι : Type u_1
α : Type u_2
β : Type u_3
a : α
s✝ t : Set α
x u v : Set (α × α)
inst✝ : UniformSpace α
s : Set α
⊢ 𝓝ˢ s ≤ 𝓝ᵘ s
Tactic:
simpa [nhdsSet] using λ _ => nhds_le_uniform_nhds_set
Proof state after:
no goals
Theorem: UniformSpace.uniform_nhds_inf_uniform_nhds_eq_bot
Proof state before:
ι : Type u_1
α : Type u_2
β : Type u_3
a : α
s✝ t✝ : Set α
x u v : Set (α × α)
inst✝ : UniformSpace α
s t : Set α
h : 𝓝ᵘ s ⊓ 𝓟 t = ⊥
⊢ 𝓝ᵘ s ⊓ 𝓝ᵘ t = ⊥
Tactic:
simp_rw [inf_principal_eq_bot, inf_eq_bot_iff, mem_uniform_nhds_set_iff] at h ⊢
Proof state after:
ι : Type u_1
α : Type u_2
β : Type u_3
a : α
s✝ t✝ : Set α
x u v : Set (α × α)
inst✝ : UniformSpace α
s t : Set α
h : ∃ u ∈ 𝓤 α, thickening u s ⊆ tᶜ
⊢ ∃ U, (∃ u ∈ 𝓤 α, thickening u s ⊆ U) ∧ ∃ V, (∃ u ∈ 𝓤 α, thickening u t ⊆ V) ∧ U ∩ V = ∅
Theorem: UniformSpace.uniform_nhds_inf_uniform_nhds_eq_bot
Proof state before:
ι : Type u_1
α : Type u_2
β : Type u_3
a : α
s✝ t✝ : Set α
x u v : Set (α × α)
inst✝ : UniformSpace α
s t : Set α
h : ∃ u ∈ 𝓤 α, thickening u s ⊆ tᶜ
⊢ ∃ U, (∃ u ∈ 𝓤 α, thickening u s ⊆ U) ∧ ∃ V, (∃ u ∈ 𝓤 α, thickening u t ⊆ V) ∧ U ∩ V = ∅
Tactic:
obtain ⟨u, hu, hsu⟩ := h
Proof state after:
case intro.intro
ι : Type u_1
α : Type u_2
β : Type u_3
a : α
s✝ t✝ : Set α
x u✝ v : Set (α × α)
inst✝ : UniformSpace α
s t : Set α
u : Set (α × α)
hu : u ∈ 𝓤 α
hsu : thickening u s ⊆ tᶜ
⊢ ∃ U, (∃ u ∈ 𝓤 α, thickening u s ⊆ U) ∧ ∃ V, (∃ u ∈ 𝓤 α, thickening u t ⊆ V) ∧ U ∩ V = ∅
Theorem: UniformSpace.uniform_nhds_inf_uniform_nhds_eq_bot
Proof state before:
case intro.intro
ι : Type u_1
α : Type u_2
β : Type u_3
a : α
s✝ t✝ : Set α
x u✝ v : Set (α × α)
inst✝ : UniformSpace α
s t : Set α
u : Set (α × α)
hu : u ∈ 𝓤 α
hsu : thickening u s ⊆ tᶜ
⊢ ∃ U, (∃ u ∈ 𝓤 α, thickening u s ⊆ U) ∧ ∃ V, (∃ u ∈ 𝓤 α, thickening u t ⊆ V) ∧ U ∩ V = ∅
Tactic:
obtain ⟨v, hv, hvs, hvu⟩ := comp_symm_of_uniformity hu
Proof state after:
case intro.intro.intro.intro.intro
ι : Type u_1
α : Type u_2
β : Type u_3
a : α
s✝ t✝ : Set α
x u✝ v✝ : Set (α × α)
inst✝ : UniformSpace α
s t : Set α
u : Set (α × α)
hu : u ∈ 𝓤 α
hsu : thickening u s ⊆ tᶜ
v : Set (α × α)
hv : v ∈ 𝓤 α
hvs : ∀ {a b : α}, (a, b) ∈ v → (b, a) ∈ v
hvu : v ○ v ⊆ u
⊢ ∃ U, (∃ u ∈ 𝓤 α, thickening u s ⊆ U) ∧ ∃ V, (∃ u ∈ 𝓤 α, thickening u t ⊆ V) ∧ U ∩ V = ∅
Theorem: UniformSpace.uniform_nhds_inf_uniform_nhds_eq_bot
Proof state before:
case intro.intro.intro.intro.intro
ι : Type u_1
α : Type u_2
β : Type u_3
a : α
s✝ t✝ : Set α
x u✝ v✝ : Set (α × α)
inst✝ : UniformSpace α
s t : Set α
u : Set (α × α)
hu : u ∈ 𝓤 α
hsu : thickening u s ⊆ tᶜ
v : Set (α × α)
hv : v ∈ 𝓤 α
hvs : ∀ {a b : α}, (a, b) ∈ v → (b, a) ∈ v
hvu : v ○ v ⊆ u
⊢ ∃ U, (∃ u ∈ 𝓤 α, thickening u s ⊆ U) ∧ ∃ V, (∃ u ∈ 𝓤 α, thickening u t ⊆ V) ∧ U ∩ V = ∅
Tactic:
refine ⟨_, ⟨v, hv, subset_rfl⟩, _, ⟨v, hv, subset_rfl⟩, ?h⟩
Proof state after:
case h
ι : Type u_1
α : Type u_2
β : Type u_3
a : α
s✝ t✝ : Set α
x u✝ v✝ : Set (α × α)
inst✝ : UniformSpace α
s t : Set α
u : Set (α × α)
hu : u ∈ 𝓤 α
hsu : thickening u s ⊆ tᶜ
v : Set (α × α)
hv : v ∈ 𝓤 α
hvs : ∀ {a b : α}, (a, b) ∈ v → (b, a) ∈ v
hvu : v ○ v ⊆ u
⊢ thickening v s ∩ thickening v t = ∅
Theorem: UniformSpace.uniform_nhds_inf_uniform_nhds_eq_bot
Proof state before:
case h
ι : Type u_1
α : Type u_2
β : Type u_3
a : α
s✝ t✝ : Set α
x u✝ v✝ : Set (α × α)
inst✝ : UniformSpace α
s t : Set α
u : Set (α × α)
hu : u ∈ 𝓤 α
hsu : thickening u s ⊆ tᶜ
v : Set (α × α)
hv : v ∈ 𝓤 α
hvs : ∀ {a b : α}, (a, b) ∈ v → (b, a) ∈ v
hvu : v ○ v ⊆ u
⊢ thickening v s ∩ thickening v t = ∅
Tactic:
apply thickening_inter_thickening_eq_empty_of_comp (symmetricRel_of hvs) hvu
Proof state after:
case h
ι : Type u_1
α : Type u_2
β : Type u_3
a : α
s✝ t✝ : Set α
x u✝ v✝ : Set (α × α)
inst✝ : UniformSpace α
s t : Set α
u : Set (α × α)
hu : u ∈ 𝓤 α
hsu : thickening u s ⊆ tᶜ
v : Set (α × α)
hv : v ∈ 𝓤 α
hvs : ∀ {a b : α}, (a, b) ∈ v → (b, a) ∈ v
hvu : v ○ v ⊆ u
⊢ thickening u s ∩ t = ∅
Theorem: UniformSpace.uniform_nhds_inf_uniform_nhds_eq_bot
Proof state before:
case h
ι : Type u_1
α : Type u_2
β : Type u_3
a : α
s✝ t✝ : Set α
x u✝ v✝ : Set (α × α)
inst✝ : UniformSpace α
s t : Set α
u : Set (α × α)
hu : u ∈ 𝓤 α
hsu : thickening u s ⊆ tᶜ
v : Set (α × α)
hv : v ∈ 𝓤 α
hvs : ∀ {a b : α}, (a, b) ∈ v → (b, a) ∈ v
hvu : v ○ v ⊆ u
⊢ thickening u s ∩ t = ∅
Tactic:
exact (subset_compl_iff_disjoint_right.mp hsu).inter_eq
Proof state after:
no goals
Theorem: UniformSpace.nhds_inf_uniform_nhds_eq_bot
Proof state before:
ι : Type u_1
α : Type u_2
β : Type u_3
a : α
s✝ t : Set α
x u v : Set (α × α)
inst✝ : UniformSpace α
s : Set α
hf : 𝓝 a ⊓ 𝓟 s = ⊥
⊢ 𝓝 a ⊓ 𝓝ᵘ s = ⊥
Tactic:
rw [← uniform_nhds_set_singleton] at hf ⊢
Proof state after:
ι : Type u_1
α : Type u_2
β : Type u_3
a : α
s✝ t : Set α
x u v : Set (α × α)
inst✝ : UniformSpace α
s : Set α
hf : 𝓝ᵘ {a} ⊓ 𝓟 s = ⊥
⊢ 𝓝ᵘ {a} ⊓ 𝓝ᵘ s = ⊥
Theorem: UniformSpace.nhds_inf_uniform_nhds_eq_bot
Proof state before:
ι : Type u_1
α : Type u_2
β : Type u_3
a : α
s✝ t : Set α
x u v : Set (α × α)
inst✝ : UniformSpace α
s : Set α
hf : 𝓝ᵘ {a} ⊓ 𝓟 s = ⊥
⊢ 𝓝ᵘ {a} ⊓ 𝓝ᵘ s = ⊥
Tactic:
exact uniform_nhds_inf_uniform_nhds_eq_bot hf
Proof state after:
no goals
Theorem: lemma0
Proof state before:
ι : Type u_1
α : Type u_2
β : Type u_3
a : α
s t : Set α
x u v : Set (α × α)
p : Filter ι
inst✝ : UniformSpace α
⊢ Tendsto Prod.snd (𝓤 α ⊓ Filter.comap Prod.fst (𝓟 s)) (𝓝ᵘ s)
Tactic:
simp_rw [comap_principal, uniform_nhds_set, tendsto_lift', eventually_inf_principal]
Proof state after:
ι : Type u_1
α : Type u_2
β : Type u_3
a : α
s t : Set α
x u v : Set (α × α)
p : Filter ι
inst✝ : UniformSpace α
⊢ ∀ s_1 ∈ 𝓤 α, ∀ᶠ (x : α × α) in 𝓤 α, x ∈ Prod.fst ⁻¹' s → x.2 ∈ thickening s_1 s
Theorem: lemma0
Proof state before:
ι : Type u_1
α : Type u_2
β : Type u_3
a : α
s t : Set α
x u v : Set (α × α)
p : Filter ι
inst✝ : UniformSpace α
⊢ ∀ s_1 ∈ 𝓤 α, ∀ᶠ (x : α × α) in 𝓤 α, x ∈ Prod.fst ⁻¹' s → x.2 ∈ thickening s_1 s
Tactic:
exact λ U hU => mem_of_superset hU (λ ⟨x, y⟩ hxy hx => mem_biUnion hx hxy)
Proof state after:
no goals
Theorem: lemma1
Proof state before:
ι : Type u_1
α : Type u_2
β : Type u_3
a : α
s t : Set α
x u v : Set (α × α)
p : Filter ι
F : ι → α → β
f : α → β
inst✝ : UniformSpace β
hF : TendstoUniformlyOn F f p s
⊢ Tendsto (fun q => (f q.2, F q.1 q.2)) (p ×ˢ 𝓟 s) (𝓟 (f '' s) ×ˢ 𝓝ᵘ (f '' s))
Tactic:
rw [tendstoUniformlyOn_iff_tendsto] at hF
Proof state after:
ι : Type u_1
α : Type u_2
β : Type u_3
a : α
s t : Set α
x u v : Set (α × α)
p : Filter ι
F : ι → α → β
f : α → β
inst✝ : UniformSpace β
hF : Tendsto (fun q => (f q.2, F q.1 q.2)) (p ×ˢ 𝓟 s) (𝓤 β)
⊢ Tendsto (fun q => (f q.2, F q.1 q.2)) (p ×ˢ 𝓟 s) (𝓟 (f '' s) ×ˢ 𝓝ᵘ (f '' s))