internlm/Lean-Github huggingface dataset:
Theorem: tendsto_atInf_iff_tendsto_nhds_zero
Proof state before:
case h
𝕜 X : Type
inst✝ : NontriviallyNormedField 𝕜
l : Filter X
f : 𝕜 → X
h : ∀ t ∈ l, ∃ i, True ∧ MapsTo f {x | i < ‖x‖} t
t : Set X
tl : t ∈ l
r : ℝ
left✝ : True
m : MapsTo f {x | r < ‖x‖} t
rp : ¬0 < r
⊢ MapsTo (fun x => f x⁻¹) (ball 0 1 ∩ {0}ᶜ) t
Tactic:
intro x xs
Proof state after:
case h
𝕜 X : Type
inst✝ : NontriviallyNormedField 𝕜
l : Filter X
f : 𝕜 → X
h : ∀ t ∈ l, ∃ i, True ∧ MapsTo f {x | i < ‖x‖} t
t : Set X
tl : t ∈ l
r : ℝ
left✝ : True
m : MapsTo f {x | r < ‖x‖} t
rp : ¬0 < r
x : 𝕜
xs : x ∈ ball 0 1 ∩ {0}ᶜ
⊢ (fun x => f x⁻¹) x ∈ t
Theorem: tendsto_atInf_iff_tendsto_nhds_zero
Proof state before:
case h
𝕜 X : Type
inst✝ : NontriviallyNormedField 𝕜
l : Filter X
f : 𝕜 → X
h : ∀ t ∈ l, ∃ i, True ∧ MapsTo f {x | i < ‖x‖} t
t : Set X
tl : t ∈ l
r : ℝ
left✝ : True
m : MapsTo f {x | r < ‖x‖} t
rp : ¬0 < r
x : 𝕜
xs : x ∈ ball 0 1 ∩ {0}ᶜ
⊢ (fun x => f x⁻¹) x ∈ t
Tactic:
refine m ?_
Proof state after:
case h
𝕜 X : Type
inst✝ : NontriviallyNormedField 𝕜
l : Filter X
f : 𝕜 → X
h : ∀ t ∈ l, ∃ i, True ∧ MapsTo f {x | i < ‖x‖} t
t : Set X
tl : t ∈ l
r : ℝ
left✝ : True
m : MapsTo f {x | r < ‖x‖} t
rp : ¬0 < r
x : 𝕜
xs : x ∈ ball 0 1 ∩ {0}ᶜ
⊢ x⁻¹ ∈ {x | r < ‖x‖}
Theorem: tendsto_atInf_iff_tendsto_nhds_zero
Proof state before:
case h
𝕜 X : Type
inst✝ : NontriviallyNormedField 𝕜
l : Filter X
f : 𝕜 → X
h : ∀ t ∈ l, ∃ i, True ∧ MapsTo f {x | i < ‖x‖} t
t : Set X
tl : t ∈ l
r : ℝ
left✝ : True
m : MapsTo f {x | r < ‖x‖} t
rp : ¬0 < r
x : 𝕜
xs : x ∈ ball 0 1 ∩ {0}ᶜ
⊢ x⁻¹ ∈ {x | r < ‖x‖}
Tactic:
simp only [mem_inter_iff, mem_ball_zero_iff, mem_compl_iff, mem_singleton_iff] at xs
Proof state after:
case h
𝕜 X : Type
inst✝ : NontriviallyNormedField 𝕜
l : Filter X
f : 𝕜 → X
h : ∀ t ∈ l, ∃ i, True ∧ MapsTo f {x | i < ‖x‖} t
t : Set X
tl : t ∈ l
r : ℝ
left✝ : True
m : MapsTo f {x | r < ‖x‖} t
rp : ¬0 < r
x : 𝕜
xs : ‖x‖ < 1 ∧ ¬x = 0
⊢ x⁻¹ ∈ {x | r < ‖x‖}
Theorem: tendsto_atInf_iff_tendsto_nhds_zero
Proof state before:
case h
𝕜 X : Type
inst✝ : NontriviallyNormedField 𝕜
l : Filter X
f : 𝕜 → X
h : ∀ t ∈ l, ∃ i, True ∧ MapsTo f {x | i < ‖x‖} t
t : Set X
tl : t ∈ l
r : ℝ
left✝ : True
m : MapsTo f {x | r < ‖x‖} t
rp : ¬0 < r
x : 𝕜
xs : ‖x‖ < 1 ∧ ¬x = 0
⊢ x⁻¹ ∈ {x | r < ‖x‖}
Tactic:
simp only [mem_setOf_eq, norm_inv]
Proof state after:
case h
𝕜 X : Type
inst✝ : NontriviallyNormedField 𝕜
l : Filter X
f : 𝕜 → X
h : ∀ t ∈ l, ∃ i, True ∧ MapsTo f {x | i < ‖x‖} t
t : Set X
tl : t ∈ l
r : ℝ
left✝ : True
m : MapsTo f {x | r < ‖x‖} t
rp : ¬0 < r
x : 𝕜
xs : ‖x‖ < 1 ∧ ¬x = 0
⊢ r < ‖x‖⁻¹
Theorem: tendsto_atInf_iff_tendsto_nhds_zero
Proof state before:
case h
𝕜 X : Type
inst✝ : NontriviallyNormedField 𝕜
l : Filter X
f : 𝕜 → X
h : ∀ t ∈ l, ∃ i, True ∧ MapsTo f {x | i < ‖x‖} t
t : Set X
tl : t ∈ l
r : ℝ
left✝ : True
m : MapsTo f {x | r < ‖x‖} t
rp : ¬0 < r
x : 𝕜
xs : ‖x‖ < 1 ∧ ¬x = 0
⊢ r < ‖x‖⁻¹
Tactic:
simp only [not_lt] at rp
Proof state after:
case h
𝕜 X : Type
inst✝ : NontriviallyNormedField 𝕜
l : Filter X
f : 𝕜 → X
h : ∀ t ∈ l, ∃ i, True ∧ MapsTo f {x | i < ‖x‖} t
t : Set X
tl : t ∈ l
r : ℝ
left✝ : True
m : MapsTo f {x | r < ‖x‖} t
x : 𝕜
xs : ‖x‖ < 1 ∧ ¬x = 0
rp : r ≤ 0
⊢ r < ‖x‖⁻¹
Theorem: tendsto_atInf_iff_tendsto_nhds_zero
Proof state before:
case h
𝕜 X : Type
inst✝ : NontriviallyNormedField 𝕜
l : Filter X
f : 𝕜 → X
h : ∀ t ∈ l, ∃ i, True ∧ MapsTo f {x | i < ‖x‖} t
t : Set X
tl : t ∈ l
r : ℝ
left✝ : True
m : MapsTo f {x | r < ‖x‖} t
x : 𝕜
xs : ‖x‖ < 1 ∧ ¬x = 0
rp : r ≤ 0
⊢ r < ‖x‖⁻¹
Tactic:
exact lt_of_le_of_lt rp (inv_pos.mpr (norm_pos_iff.mpr xs.2))
Proof state after:
no goals
Theorem: tendsto_atInf_iff_tendsto_nhds_zero
Proof state before:
case mpr
𝕜 X : Type
inst✝ : NontriviallyNormedField 𝕜
l : Filter X
f : 𝕜 → X
⊢ (∀ t ∈ l, ∃ i, 0 < i ∧ MapsTo (fun x => f x⁻¹) (ball 0 i ∩ {0}ᶜ) t) → ∀ t ∈ l, ∃ i, True ∧ MapsTo f {x | i < ‖x‖} t
Tactic:
intro h t tl
Proof state after:
case mpr
𝕜 X : Type
inst✝ : NontriviallyNormedField 𝕜
l : Filter X
f : 𝕜 → X
h : ∀ t ∈ l, ∃ i, 0 < i ∧ MapsTo (fun x => f x⁻¹) (ball 0 i ∩ {0}ᶜ) t
t : Set X
tl : t ∈ l
⊢ ∃ i, True ∧ MapsTo f {x | i < ‖x‖} t
Theorem: tendsto_atInf_iff_tendsto_nhds_zero
Proof state before:
case mpr
𝕜 X : Type
inst✝ : NontriviallyNormedField 𝕜
l : Filter X
f : 𝕜 → X
h : ∀ t ∈ l, ∃ i, 0 < i ∧ MapsTo (fun x => f x⁻¹) (ball 0 i ∩ {0}ᶜ) t
t : Set X
tl : t ∈ l
⊢ ∃ i, True ∧ MapsTo f {x | i < ‖x‖} t
Tactic:
rcases h t tl with ⟨r, rp, m⟩
Proof state after:
case mpr.intro.intro
𝕜 X : Type
inst✝ : NontriviallyNormedField 𝕜
l : Filter X
f : 𝕜 → X
h : ∀ t ∈ l, ∃ i, 0 < i ∧ MapsTo (fun x => f x⁻¹) (ball 0 i ∩ {0}ᶜ) t
t : Set X
tl : t ∈ l
r : ℝ
rp : 0 < r
m : MapsTo (fun x => f x⁻¹) (ball 0 r ∩ {0}ᶜ) t
⊢ ∃ i, True ∧ MapsTo f {x | i < ‖x‖} t
Theorem: tendsto_atInf_iff_tendsto_nhds_zero
Proof state before:
case mpr.intro.intro
𝕜 X : Type
inst✝ : NontriviallyNormedField 𝕜
l : Filter X
f : 𝕜 → X
h : ∀ t ∈ l, ∃ i, 0 < i ∧ MapsTo (fun x => f x⁻¹) (ball 0 i ∩ {0}ᶜ) t
t : Set X
tl : t ∈ l
r : ℝ
rp : 0 < r
m : MapsTo (fun x => f x⁻¹) (ball 0 r ∩ {0}ᶜ) t
⊢ ∃ i, True ∧ MapsTo f {x | i < ‖x‖} t
Tactic:
use r⁻¹
Proof state after:
case h
𝕜 X : Type
inst✝ : NontriviallyNormedField 𝕜
l : Filter X
f : 𝕜 → X
h : ∀ t ∈ l, ∃ i, 0 < i ∧ MapsTo (fun x => f x⁻¹) (ball 0 i ∩ {0}ᶜ) t
t : Set X
tl : t ∈ l
r : ℝ
rp : 0 < r
m : MapsTo (fun x => f x⁻¹) (ball 0 r ∩ {0}ᶜ) t
⊢ True ∧ MapsTo f {x | r⁻¹ < ‖x‖} t
Theorem: tendsto_atInf_iff_tendsto_nhds_zero
Proof state before:
case h
𝕜 X : Type
inst✝ : NontriviallyNormedField 𝕜
l : Filter X
f : 𝕜 → X
h : ∀ t ∈ l, ∃ i, 0 < i ∧ MapsTo (fun x => f x⁻¹) (ball 0 i ∩ {0}ᶜ) t
t : Set X
tl : t ∈ l
r : ℝ
rp : 0 < r
m : MapsTo (fun x => f x⁻¹) (ball 0 r ∩ {0}ᶜ) t
⊢ True ∧ MapsTo f {x | r⁻¹ < ‖x‖} t
Tactic:
simp only [true_and_iff]
Proof state after:
case h
𝕜 X : Type
inst✝ : NontriviallyNormedField 𝕜
l : Filter X
f : 𝕜 → X
h : ∀ t ∈ l, ∃ i, 0 < i ∧ MapsTo (fun x => f x⁻¹) (ball 0 i ∩ {0}ᶜ) t
t : Set X
tl : t ∈ l
r : ℝ
rp : 0 < r
m : MapsTo (fun x => f x⁻¹) (ball 0 r ∩ {0}ᶜ) t
⊢ MapsTo f {x | r⁻¹ < ‖x‖} t
Theorem: tendsto_atInf_iff_tendsto_nhds_zero
Proof state before:
case h
𝕜 X : Type
inst✝ : NontriviallyNormedField 𝕜
l : Filter X
f : 𝕜 → X
h : ∀ t ∈ l, ∃ i, 0 < i ∧ MapsTo (fun x => f x⁻¹) (ball 0 i ∩ {0}ᶜ) t
t : Set X
tl : t ∈ l
r : ℝ
rp : 0 < r
m : MapsTo (fun x => f x⁻¹) (ball 0 r ∩ {0}ᶜ) t
⊢ MapsTo f {x | r⁻¹ < ‖x‖} t
Tactic:
intro x xs
Proof state after:
case h
𝕜 X : Type
inst✝ : NontriviallyNormedField 𝕜
l : Filter X
f : 𝕜 → X
h : ∀ t ∈ l, ∃ i, 0 < i ∧ MapsTo (fun x => f x⁻¹) (ball 0 i ∩ {0}ᶜ) t
t : Set X
tl : t ∈ l
r : ℝ
rp : 0 < r
m : MapsTo (fun x => f x⁻¹) (ball 0 r ∩ {0}ᶜ) t
x : 𝕜
xs : x ∈ {x | r⁻¹ < ‖x‖}
⊢ f x ∈ t
Theorem: tendsto_atInf_iff_tendsto_nhds_zero
Proof state before:
case h
𝕜 X : Type
inst✝ : NontriviallyNormedField 𝕜
l : Filter X
f : 𝕜 → X
h : ∀ t ∈ l, ∃ i, 0 < i ∧ MapsTo (fun x => f x⁻¹) (ball 0 i ∩ {0}ᶜ) t
t : Set X
tl : t ∈ l
r : ℝ
rp : 0 < r
m : MapsTo (fun x => f x⁻¹) (ball 0 r ∩ {0}ᶜ) t
x : 𝕜
xs : x ∈ {x | r⁻¹ < ‖x‖}
⊢ f x ∈ t
Tactic:
simp only [mem_setOf_eq] at xs
Proof state after:
case h
𝕜 X : Type
inst✝ : NontriviallyNormedField 𝕜
l : Filter X
f : 𝕜 → X
h : ∀ t ∈ l, ∃ i, 0 < i ∧ MapsTo (fun x => f x⁻¹) (ball 0 i ∩ {0}ᶜ) t
t : Set X
tl : t ∈ l
r : ℝ
rp : 0 < r
m : MapsTo (fun x => f x⁻¹) (ball 0 r ∩ {0}ᶜ) t
x : 𝕜
xs : r⁻¹ < ‖x‖
⊢ f x ∈ t
Theorem: tendsto_atInf_iff_tendsto_nhds_zero
Proof state before:
case h
𝕜 X : Type
inst✝ : NontriviallyNormedField 𝕜
l : Filter X
f : 𝕜 → X
h : ∀ t ∈ l, ∃ i, 0 < i ∧ MapsTo (fun x => f x⁻¹) (ball 0 i ∩ {0}ᶜ) t
t : Set X
tl : t ∈ l
r : ℝ
rp : 0 < r
m : MapsTo (fun x => f x⁻¹) (ball 0 r ∩ {0}ᶜ) t
x : 𝕜
xs : r⁻¹ < ‖x‖
⊢ f x ∈ t
Tactic:
have m := @m x⁻¹ ?_
Proof state after:
case h.refine_2
𝕜 X : Type
inst✝ : NontriviallyNormedField 𝕜
l : Filter X
f : 𝕜 → X
h : ∀ t ∈ l, ∃ i, 0 < i ∧ MapsTo (fun x => f x⁻¹) (ball 0 i ∩ {0}ᶜ) t
t : Set X
tl : t ∈ l
r : ℝ
rp : 0 < r
m✝ : MapsTo (fun x => f x⁻¹) (ball 0 r ∩ {0}ᶜ) t
x : 𝕜
xs : r⁻¹ < ‖x‖
m : (fun x => f x⁻¹) x⁻¹ ∈ t
⊢ f x ∈ t

case h.refine_1
𝕜 X : Type
inst✝ : NontriviallyNormedField 𝕜
l : Filter X
f : 𝕜 → X
h : ∀ t ∈ l, ∃ i, 0 < i ∧ MapsTo (fun x => f x⁻¹) (ball 0 i ∩ {0}ᶜ) t
t : Set X
tl : t ∈ l
r : ℝ
rp : 0 < r
m : MapsTo (fun x => f x⁻¹) (ball 0 r ∩ {0}ᶜ) t
x : 𝕜
xs : r⁻¹ < ‖x‖
⊢ x⁻¹ ∈ ball 0 r ∩ {0}ᶜ
Theorem: tendsto_atInf_iff_tendsto_nhds_zero
Proof state before:
case h.refine_1
𝕜 X : Type
inst✝ : NontriviallyNormedField 𝕜
l : Filter X
f : 𝕜 → X
h : ∀ t ∈ l, ∃ i, 0 < i ∧ MapsTo (fun x => f x⁻¹) (ball 0 i ∩ {0}ᶜ) t
t : Set X
tl : t ∈ l
r : ℝ
rp : 0 < r
m : MapsTo (fun x => f x⁻¹) (ball 0 r ∩ {0}ᶜ) t
x : 𝕜
xs : r⁻¹ < ‖x‖
⊢ x⁻¹ ∈ ball 0 r ∩ {0}ᶜ
Tactic:
simp only [mem_inter_iff, mem_ball_zero_iff, norm_inv, mem_compl_iff, mem_singleton_iff,
  inv_eq_zero]
Proof state after:
case h.refine_1
𝕜 X : Type
inst✝ : NontriviallyNormedField 𝕜
l : Filter X
f : 𝕜 → X
h : ∀ t ∈ l, ∃ i, 0 < i ∧ MapsTo (fun x => f x⁻¹) (ball 0 i ∩ {0}ᶜ) t
t : Set X
tl : t ∈ l
r : ℝ
rp : 0 < r
m : MapsTo (fun x => f x⁻¹) (ball 0 r ∩ {0}ᶜ) t
x : 𝕜
xs : r⁻¹ < ‖x‖
⊢ ‖x‖⁻¹ < r ∧ ¬x = 0
Theorem: tendsto_atInf_iff_tendsto_nhds_zero
Proof state before:
case h.refine_1
𝕜 X : Type
inst✝ : NontriviallyNormedField 𝕜
l : Filter X
f : 𝕜 → X
h : ∀ t ∈ l, ∃ i, 0 < i ∧ MapsTo (fun x => f x⁻¹) (ball 0 i ∩ {0}ᶜ) t
t : Set X
tl : t ∈ l
r : ℝ
rp : 0 < r
m : MapsTo (fun x => f x⁻¹) (ball 0 r ∩ {0}ᶜ) t
x : 𝕜
xs : r⁻¹ < ‖x‖
⊢ ‖x‖⁻¹ < r ∧ ¬x = 0
Tactic:
have np : 0 < ‖x‖ := _root_.trans (inv_pos.mpr rp) xs
Proof state after:
case h.refine_1
𝕜 X : Type
inst✝ : NontriviallyNormedField 𝕜
l : Filter X
f : 𝕜 → X
h : ∀ t ∈ l, ∃ i, 0 < i ∧ MapsTo (fun x => f x⁻¹) (ball 0 i ∩ {0}ᶜ) t
t : Set X
tl : t ∈ l
r : ℝ
rp : 0 < r
m : MapsTo (fun x => f x⁻¹) (ball 0 r ∩ {0}ᶜ) t
x : 𝕜
xs : r⁻¹ < ‖x‖
np : 0 < ‖x‖
⊢ ‖x‖⁻¹ < r ∧ ¬x = 0
Theorem: tendsto_atInf_iff_tendsto_nhds_zero
Proof state before:
case h.refine_1
𝕜 X : Type
inst✝ : NontriviallyNormedField 𝕜
l : Filter X
f : 𝕜 → X
h : ∀ t ∈ l, ∃ i, 0 < i ∧ MapsTo (fun x => f x⁻¹) (ball 0 i ∩ {0}ᶜ) t
t : Set X
tl : t ∈ l
r : ℝ
rp : 0 < r
m : MapsTo (fun x => f x⁻¹) (ball 0 r ∩ {0}ᶜ) t
x : 𝕜
xs : r⁻¹ < ‖x‖
np : 0 < ‖x‖
⊢ ‖x‖⁻¹ < r ∧ ¬x = 0
Tactic:
simp [inv_lt np rp, xs, norm_pos_iff.mp np]
Proof state after:
no goals
Theorem: tendsto_atInf_iff_tendsto_nhds_zero
Proof state before:
case h.refine_2
𝕜 X : Type
inst✝ : NontriviallyNormedField 𝕜
l : Filter X
f : 𝕜 → X
h : ∀ t ∈ l, ∃ i, 0 < i ∧ MapsTo (fun x => f x⁻¹) (ball 0 i ∩ {0}ᶜ) t
t : Set X
tl : t ∈ l
r : ℝ
rp : 0 < r
m✝ : MapsTo (fun x => f x⁻¹) (ball 0 r ∩ {0}ᶜ) t
x : 𝕜
xs : r⁻¹ < ‖x‖
m : (fun x => f x⁻¹) x⁻¹ ∈ t
⊢ f x ∈ t
Tactic:
simp only [inv_inv] at m
Proof state after:
case h.refine_2
𝕜 X : Type
inst✝ : NontriviallyNormedField 𝕜
l : Filter X
f : 𝕜 → X
h : ∀ t ∈ l, ∃ i, 0 < i ∧ MapsTo (fun x => f x⁻¹) (ball 0 i ∩ {0}ᶜ) t
t : Set X
tl : t ∈ l
r : ℝ
rp : 0 < r
m✝ : MapsTo (fun x => f x⁻¹) (ball 0 r ∩ {0}ᶜ) t
x : 𝕜
xs : r⁻¹ < ‖x‖
m : f x ∈ t
⊢ f x ∈ t
Theorem: tendsto_atInf_iff_tendsto_nhds_zero
Proof state before:
case h.refine_2
𝕜 X : Type
inst✝ : NontriviallyNormedField 𝕜
l : Filter X
f : 𝕜 → X
h : ∀ t ∈ l, ∃ i, 0 < i ∧ MapsTo (fun x => f x⁻¹) (ball 0 i ∩ {0}ᶜ) t
t : Set X
tl : t ∈ l
r : ℝ
rp : 0 < r
m✝ : MapsTo (fun x => f x⁻¹) (ball 0 r ∩ {0}ᶜ) t
x : 𝕜
xs : r⁻¹ < ‖x‖
m : f x ∈ t
⊢ f x ∈ t
Tactic:
exact m
Proof state after:
no goals
Theorem: atInf_le_cocompact
Proof state before:
X : Type
inst✝ : NormedAddCommGroup X
⊢ atInf ≤ Filter.cocompact X
Tactic:
rw [Filter.le_def]
Proof state after:
X : Type
inst✝ : NormedAddCommGroup X
⊢ ∀ x ∈ Filter.cocompact X, x ∈ atInf
Theorem: atInf_le_cocompact
Proof state before:
X : Type
inst✝ : NormedAddCommGroup X
⊢ ∀ x ∈ Filter.cocompact X, x ∈ atInf
Tactic:
intro s m
Proof state after:
X : Type
inst✝ : NormedAddCommGroup X
s : Set X
m : s ∈ Filter.cocompact X
⊢ s ∈ atInf
Theorem: atInf_le_cocompact
Proof state before:
X : Type
inst✝ : NormedAddCommGroup X
s : Set X
m : s ∈ Filter.cocompact X
⊢ s ∈ atInf
Tactic:
rcases Filter.mem_cocompact.mp m with ⟨t, tc, ts⟩
Proof state after:
case intro.intro
X : Type
inst✝ : NormedAddCommGroup X
s : Set X
m : s ∈ Filter.cocompact X
t : Set X
tc : IsCompact t
ts : tᶜ ⊆ s
⊢ s ∈ atInf
Theorem: atInf_le_cocompact
Proof state before:
case intro.intro
X : Type
inst✝ : NormedAddCommGroup X
s : Set X
m : s ∈ Filter.cocompact X
t : Set X
tc : IsCompact t
ts : tᶜ ⊆ s
⊢ s ∈ atInf
Tactic:
rcases tc.bddAbove_image continuousOn_id.norm with ⟨r, rh⟩
Proof state after:
case intro.intro.intro
X : Type
inst✝ : NormedAddCommGroup X
s : Set X
m : s ∈ Filter.cocompact X
t : Set X
tc : IsCompact t
ts : tᶜ ⊆ s
r : ℝ
rh : r ∈ upperBounds ((fun x => ‖id x‖) '' t)
⊢ s ∈ atInf
Theorem: atInf_le_cocompact
Proof state before:
case intro.intro.intro
X : Type
inst✝ : NormedAddCommGroup X
s : Set X
m : s ∈ Filter.cocompact X
t : Set X
tc : IsCompact t
ts : tᶜ ⊆ s
r : ℝ
rh : r ∈ upperBounds ((fun x => ‖id x‖) '' t)
⊢ s ∈ atInf
Tactic:
simp only [id_eq, mem_upperBounds, mem_image, forall_exists_index, and_imp,
  forall_apply_eq_imp_iff₂] at rh
Proof state after:
case intro.intro.intro
X : Type
inst✝ : NormedAddCommGroup X
s : Set X
m : s ∈ Filter.cocompact X
t : Set X
tc : IsCompact t
ts : tᶜ ⊆ s
r : ℝ
rh : ∀ a ∈ t, ‖a‖ ≤ r
⊢ s ∈ atInf
Theorem: atInf_le_cocompact
Proof state before:
case intro.intro.intro
X : Type
inst✝ : NormedAddCommGroup X
s : Set X
m : s ∈ Filter.cocompact X
t : Set X
tc : IsCompact t
ts : tᶜ ⊆ s
r : ℝ
rh : ∀ a ∈ t, ‖a‖ ≤ r
⊢ s ∈ atInf
Tactic:
rw [mem_atInf_iff]
Proof state after:
case intro.intro.intro
X : Type
inst✝ : NormedAddCommGroup X
s : Set X
m : s ∈ Filter.cocompact X
t : Set X
tc : IsCompact t
ts : tᶜ ⊆ s
r : ℝ
rh : ∀ a ∈ t, ‖a‖ ≤ r
⊢ ∃ r, {x | ‖x‖ > r} ⊆ s
Theorem: atInf_le_cocompact
Proof state before:
case intro.intro.intro
X : Type
inst✝ : NormedAddCommGroup X
s : Set X
m : s ∈ Filter.cocompact X
t : Set X
tc : IsCompact t
ts : tᶜ ⊆ s
r : ℝ
rh : ∀ a ∈ t, ‖a‖ ≤ r
⊢ ∃ r, {x | ‖x‖ > r} ⊆ s
Tactic:
use r
Proof state after:
case h
X : Type
inst✝ : NormedAddCommGroup X
s : Set X
m : s ∈ Filter.cocompact X
t : Set X
tc : IsCompact t
ts : tᶜ ⊆ s
r : ℝ
rh : ∀ a ∈ t, ‖a‖ ≤ r
⊢ {x | ‖x‖ > r} ⊆ s
Theorem: atInf_le_cocompact
Proof state before:
case h
X : Type
inst✝ : NormedAddCommGroup X
s : Set X
m : s ∈ Filter.cocompact X
t : Set X
tc : IsCompact t
ts : tᶜ ⊆ s
r : ℝ
rh : ∀ a ∈ t, ‖a‖ ≤ r
⊢ {x | ‖x‖ > r} ⊆ s
Tactic:
intro x m
Proof state after:
case h
X : Type
inst✝ : NormedAddCommGroup X
s : Set X
m✝ : s ∈ Filter.cocompact X
t : Set X
tc : IsCompact t
ts : tᶜ ⊆ s
r : ℝ
rh : ∀ a ∈ t, ‖a‖ ≤ r
x : X
m : x ∈ {x | ‖x‖ > r}
⊢ x ∈ s
Theorem: atInf_le_cocompact
Proof state before:
case h
X : Type
inst✝ : NormedAddCommGroup X
s : Set X
m✝ : s ∈ Filter.cocompact X
t : Set X
tc : IsCompact t
ts : tᶜ ⊆ s
r : ℝ
rh : ∀ a ∈ t, ‖a‖ ≤ r
x : X
m : x ∈ {x | ‖x‖ > r}
⊢ x ∈ s
Tactic:
apply ts
Proof state after:
case h.a
X : Type
inst✝ : NormedAddCommGroup X
s : Set X
m✝ : s ∈ Filter.cocompact X
t : Set X
tc : IsCompact t
ts : tᶜ ⊆ s
r : ℝ
rh : ∀ a ∈ t, ‖a‖ ≤ r
x : X
m : x ∈ {x | ‖x‖ > r}
⊢ x ∈ tᶜ
Theorem: atInf_le_cocompact
Proof state before:
case h.a
X : Type
inst✝ : NormedAddCommGroup X
s : Set X
m✝ : s ∈ Filter.cocompact X
t : Set X
tc : IsCompact t
ts : tᶜ ⊆ s
r : ℝ
rh : ∀ a ∈ t, ‖a‖ ≤ r
x : X
m : x ∈ {x | ‖x‖ > r}
⊢ x ∈ tᶜ
Tactic:
contrapose m
Proof state after:
case h.a
X : Type
inst✝ : NormedAddCommGroup X
s : Set X
m✝ : s ∈ Filter.cocompact X
t : Set X
tc : IsCompact t
ts : tᶜ ⊆ s
r : ℝ
rh : ∀ a ∈ t, ‖a‖ ≤ r
x : X
m : x ∉ tᶜ
⊢ x ∉ {x | ‖x‖ > r}
Theorem: atInf_le_cocompact
Proof state before:
case h.a
X : Type
inst✝ : NormedAddCommGroup X
s : Set X
m✝ : s ∈ Filter.cocompact X
t : Set X
tc : IsCompact t
ts : tᶜ ⊆ s
r : ℝ
rh : ∀ a ∈ t, ‖a‖ ≤ r
x : X
m : x ∉ tᶜ
⊢ x ∉ {x | ‖x‖ > r}
Tactic:
simp only [mem_compl_iff, not_not_mem] at m
Proof state after:
case h.a
X : Type
inst✝ : NormedAddCommGroup X
s : Set X
m✝ : s ∈ Filter.cocompact X
t : Set X
tc : IsCompact t
ts : tᶜ ⊆ s
r : ℝ
rh : ∀ a ∈ t, ‖a‖ ≤ r
x : X
m : x ∈ t
⊢ x ∉ {x | ‖x‖ > r}
Theorem: atInf_le_cocompact
Proof state before:
case h.a
X : Type
inst✝ : NormedAddCommGroup X
s : Set X
m✝ : s ∈ Filter.cocompact X
t : Set X
tc : IsCompact t
ts : tᶜ ⊆ s
r : ℝ
rh : ∀ a ∈ t, ‖a‖ ≤ r
x : X
m : x ∈ t
⊢ x ∉ {x | ‖x‖ > r}
Tactic:
simp only [mem_setOf_eq, not_lt]
Proof state after:
case h.a
X : Type
inst✝ : NormedAddCommGroup X
s : Set X
m✝ : s ∈ Filter.cocompact X
t : Set X
tc : IsCompact t
ts : tᶜ ⊆ s
r : ℝ
rh : ∀ a ∈ t, ‖a‖ ≤ r
x : X
m : x ∈ t
⊢ ‖x‖ ≤ r
Theorem: atInf_le_cocompact
Proof state before:
case h.a
X : Type
inst✝ : NormedAddCommGroup X
s : Set X
m✝ : s ∈ Filter.cocompact X
t : Set X
tc : IsCompact t
ts : tᶜ ⊆ s
r : ℝ
rh : ∀ a ∈ t, ‖a‖ ≤ r
x : X
m : x ∈ t
⊢ ‖x‖ ≤ r
Tactic:
exact rh _ m
Proof state after:
no goals
Theorem: atInf_eq_cocompact
Proof state before:
X : Type
inst✝¹ : NormedAddCommGroup X
inst✝ : ProperSpace X
⊢ atInf = Filter.cocompact X
Tactic:
apply le_antisymm atInf_le_cocompact
Proof state after:
X : Type
inst✝¹ : NormedAddCommGroup X
inst✝ : ProperSpace X
⊢ Filter.cocompact X ≤ atInf
Theorem: atInf_eq_cocompact
Proof state before:
X : Type
inst✝¹ : NormedAddCommGroup X
inst✝ : ProperSpace X
⊢ Filter.cocompact X ≤ atInf
Tactic:
rw [Filter.le_def]
Proof state after:
X : Type
inst✝¹ : NormedAddCommGroup X
inst✝ : ProperSpace X
⊢ ∀ x ∈ atInf, x ∈ Filter.cocompact X
Theorem: atInf_eq_cocompact
Proof state before:
X : Type
inst✝¹ : NormedAddCommGroup X
inst✝ : ProperSpace X
⊢ ∀ x ∈ atInf, x ∈ Filter.cocompact X
Tactic:
intro s m
Proof state after:
X : Type
inst✝¹ : NormedAddCommGroup X
inst✝ : ProperSpace X
s : Set X
m : s ∈ atInf
⊢ s ∈ Filter.cocompact X
Theorem: atInf_eq_cocompact
Proof state before:
X : Type
inst✝¹ : NormedAddCommGroup X
inst✝ : ProperSpace X
s : Set X
m : s ∈ atInf
⊢ s ∈ Filter.cocompact X
Tactic:
rcases mem_atInf_iff.mp m with ⟨r, h⟩
Proof state after:
case intro
X : Type
inst✝¹ : NormedAddCommGroup X
inst✝ : ProperSpace X
s : Set X
m : s ∈ atInf
r : ℝ
h : {x | ‖x‖ > r} ⊆ s
⊢ s ∈ Filter.cocompact X
Theorem: atInf_eq_cocompact
Proof state before:
case intro
X : Type
inst✝¹ : NormedAddCommGroup X
inst✝ : ProperSpace X
s : Set X
m : s ∈ atInf
r : ℝ
h : {x | ‖x‖ > r} ⊆ s
⊢ s ∈ Filter.cocompact X
Tactic:
rw [Filter.mem_cocompact]
Proof state after:
case intro
X : Type
inst✝¹ : NormedAddCommGroup X
inst✝ : ProperSpace X
s : Set X
m : s ∈ atInf
r : ℝ
h : {x | ‖x‖ > r} ⊆ s
⊢ ∃ t, IsCompact t ∧ tᶜ ⊆ s
Theorem: atInf_eq_cocompact
Proof state before:
case intro
X : Type
inst✝¹ : NormedAddCommGroup X
inst✝ : ProperSpace X
s : Set X
m : s ∈ atInf
r : ℝ
h : {x | ‖x‖ > r} ⊆ s
⊢ ∃ t, IsCompact t ∧ tᶜ ⊆ s
Tactic:
use closedBall 0 r, isCompact_closedBall _ _
Proof state after:
case right
X : Type
inst✝¹ : NormedAddCommGroup X
inst✝ : ProperSpace X
s : Set X
m : s ∈ atInf
r : ℝ
h : {x | ‖x‖ > r} ⊆ s
⊢ (closedBall 0 r)ᶜ ⊆ s
Theorem: atInf_eq_cocompact
Proof state before:
case right
X : Type
inst✝¹ : NormedAddCommGroup X
inst✝ : ProperSpace X
s : Set X
m : s ∈ atInf
r : ℝ
h : {x | ‖x‖ > r} ⊆ s
⊢ (closedBall 0 r)ᶜ ⊆ s
Tactic:
refine _root_.trans ?_ h
Proof state after:
case right
X : Type
inst✝¹ : NormedAddCommGroup X
inst✝ : ProperSpace X
s : Set X
m : s ∈ atInf
r : ℝ
h : {x | ‖x‖ > r} ⊆ s
⊢ (closedBall 0 r)ᶜ ⊆ {x | ‖x‖ > r}
Theorem: atInf_eq_cocompact
Proof state before:
case right
X : Type
inst✝¹ : NormedAddCommGroup X
inst✝ : ProperSpace X
s : Set X
m : s ∈ atInf
r : ℝ
h : {x | ‖x‖ > r} ⊆ s
⊢ (closedBall 0 r)ᶜ ⊆ {x | ‖x‖ > r}
Tactic:
intro x xs
Proof state after:
case right
X : Type
inst✝¹ : NormedAddCommGroup X
inst✝ : ProperSpace X
s : Set X
m : s ∈ atInf
r : ℝ
h : {x | ‖x‖ > r} ⊆ s
x : X
xs : x ∈ (closedBall 0 r)ᶜ
⊢ x ∈ {x | ‖x‖ > r}
Theorem: atInf_eq_cocompact
Proof state before:
case right
X : Type
inst✝¹ : NormedAddCommGroup X
inst✝ : ProperSpace X
s : Set X
m : s ∈ atInf
r : ℝ
h : {x | ‖x‖ > r} ⊆ s
x : X
xs : x ∈ (closedBall 0 r)ᶜ
⊢ x ∈ {x | ‖x‖ > r}
Tactic:
simp only [mem_compl_iff, mem_closedBall_zero_iff, not_le] at xs
Proof state after:
case right
X : Type
inst✝¹ : NormedAddCommGroup X
inst✝ : ProperSpace X
s : Set X
m : s ∈ atInf
r : ℝ
h : {x | ‖x‖ > r} ⊆ s
x : X
xs : r < ‖x‖
⊢ x ∈ {x | ‖x‖ > r}
Theorem: atInf_eq_cocompact
Proof state before:
case right
X : Type
inst✝¹ : NormedAddCommGroup X
inst✝ : ProperSpace X
s : Set X
m : s ∈ atInf
r : ℝ
h : {x | ‖x‖ > r} ⊆ s
x : X
xs : r < ‖x‖
⊢ x ∈ {x | ‖x‖ > r}
Tactic:
exact xs
Proof state after:
no goals
Theorem: inv_tendsto_atInf
Proof state before:
𝕜 : Type
inst✝ : NontriviallyNormedField 𝕜
⊢ Tendsto (fun x => x⁻¹) (𝓝[≠] 0) atInf
Tactic:
rw [←tendsto_atInf_iff_tendsto_nhds_zero (f := fun x : 𝕜 ↦ x)]
Proof state after:
𝕜 : Type
inst✝ : NontriviallyNormedField 𝕜
⊢ Tendsto (fun x => x) atInf atInf
Theorem: inv_tendsto_atInf
Proof state before:
𝕜 : Type
inst✝ : NontriviallyNormedField 𝕜
⊢ Tendsto (fun x => x) atInf atInf
Tactic:
exact Filter.tendsto_id
Proof state after:
no goals
Theorem: inv_tendsto_atInf'
Proof state before:
𝕜 : Type
inst✝ : NontriviallyNormedField 𝕜
⊢ Tendsto (fun x => x⁻¹) atInf (𝓝 0)
Tactic:
simp only [tendsto_atInf_iff_tendsto_nhds_zero, inv_inv]
Proof state after:
𝕜 : Type
inst✝ : NontriviallyNormedField 𝕜
⊢ Tendsto (fun x => x) (𝓝[≠] 0) (𝓝 0)
Theorem: inv_tendsto_atInf'
Proof state before:
𝕜 : Type
inst✝ : NontriviallyNormedField 𝕜
⊢ Tendsto (fun x => x) (𝓝[≠] 0) (𝓝 0)
Tactic:
exact Filter.tendsto_id.mono_left nhdsWithin_le_nhds
Proof state after:
no goals
Theorem: iter_large_z3
Proof state before:
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
z3 : 3 ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
n : ℕ
⊢ 2 ^ n * Complex.abs z ≤ Complex.abs ((f' d c)^[n] z)
Tactic:
rw [(by norm_num : (2:ℝ) = 3-1)]
Proof state after:
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
z3 : 3 ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
n : ℕ
⊢ (3 - 1) ^ n * Complex.abs z ≤ Complex.abs ((f' d c)^[n] z)
Theorem: iter_large_z3
Proof state before:
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
z3 : 3 ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
n : ℕ
⊢ (3 - 1) ^ n * Complex.abs z ≤ Complex.abs ((f' d c)^[n] z)
Tactic:
exact iter_large d 3 (by norm_num) z3 cz n
Proof state after:
no goals
Theorem: iter_large_z3
Proof state before:
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
z3 : 3 ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
n : ℕ
⊢ 2 = 3 - 1
Tactic:
norm_num
Proof state after:
no goals
Theorem: iter_large_z3
Proof state before:
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
z3 : 3 ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
n : ℕ
⊢ 2 ≤ 3
Tactic:
norm_num
Proof state after:
no goals
Theorem: iter_large_z4
Proof state before:
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
z4 : 4 ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
n : ℕ
⊢ 3 ^ n * Complex.abs z ≤ Complex.abs ((f' d c)^[n] z)
Tactic:
rw [(by norm_num : (3:ℝ) = 4-1)]
Proof state after:
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
z4 : 4 ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
n : ℕ
⊢ (4 - 1) ^ n * Complex.abs z ≤ Complex.abs ((f' d c)^[n] z)
Theorem: iter_large_z4
Proof state before:
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
z4 : 4 ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
n : ℕ
⊢ (4 - 1) ^ n * Complex.abs z ≤ Complex.abs ((f' d c)^[n] z)
Tactic:
exact iter_large d 4 (by norm_num) z4 cz n
Proof state after:
no goals
Theorem: iter_large_z4
Proof state before:
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
z4 : 4 ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
n : ℕ
⊢ 3 = 4 - 1
Tactic:
norm_num
Proof state after:
no goals
Theorem: iter_large_z4
Proof state before:
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
z4 : 4 ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
n : ℕ
⊢ 2 ≤ 4
Tactic:
norm_num
Proof state after:
no goals
Theorem: le_self_iter
Proof state before:
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
z3 : 3 ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
n : ℕ
⊢ Complex.abs z ≤ Complex.abs ((f' d c)^[n] z)
Tactic:
refine le_trans ?_ (iter_large_z3 d z3 cz n)
Proof state after:
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
z3 : 3 ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
n : ℕ
⊢ Complex.abs z ≤ 2 ^ n * Complex.abs z