Theorem: Csupr.has_lim (Ray/Hartogs/Duals.lean)

State before:
G : Type
inst✝³ : NormedAddCommGroup G
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : SecondCountableTopology E
s : ℕ → ℝ
ba : BddAbove (range s)
⊢ Filter.Tendsto (fun n => (partialSups s) n) atTop (𝓝 (⨆ n, s n))
Tactic:
rw [Metric.tendsto_atTop]
State after:
G : Type
inst✝³ : NormedAddCommGroup G
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : SecondCountableTopology E
s : ℕ → ℝ
ba : BddAbove (range s)
⊢ ∀ ε > 0, ∃ N, ∀ n ≥ N, dist ((partialSups s) n) (⨆ n, s n) < ε

State before:
G : Type
inst✝³ : NormedAddCommGroup G
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : SecondCountableTopology E
s : ℕ → ℝ
ba : BddAbove (range s)
⊢ ∀ ε > 0, ∃ N, ∀ n ≥ N, dist ((partialSups s) n) (⨆ n, s n) < ε
Tactic:
intro e ep
State after:
G : Type
inst✝³ : NormedAddCommGroup G
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : SecondCountableTopology E
s : ℕ → ℝ
ba : BddAbove (range s)
e : ℝ
ep : e > 0
⊢ ∃ N, ∀ n ≥ N, dist ((partialSups s) n) (⨆ n, s n) < e

State before:
G : Type
inst✝³ : NormedAddCommGroup G
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : SecondCountableTopology E
s : ℕ → ℝ
ba : BddAbove (range s)
e : ℝ
ep : e > 0
⊢ ∃ N, ∀ n ≥ N, dist ((partialSups s) n) (⨆ n, s n) < e
Tactic:
generalize hb : (⨆ n, s n) - e = b
State after:
G : Type
inst✝³ : NormedAddCommGroup G
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : SecondCountableTopology E
s : ℕ → ℝ
ba : BddAbove (range s)
e : ℝ
ep : e > 0
b : ℝ
hb : (⨆ n, s n) - e = b
⊢ ∃ N, ∀ n ≥ N, dist ((partialSups s) n) (⨆ n, s n) < e

State before:
G : Type
inst✝³ : NormedAddCommGroup G
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : SecondCountableTopology E
s : ℕ → ℝ
ba : BddAbove (range s)
e : ℝ
ep : e > 0
b : ℝ
hb : (⨆ n, s n) - e = b
⊢ ∃ N, ∀ n ≥ N, dist ((partialSups s) n) (⨆ n, s n) < e
Tactic:
have bs : b < ⨆ n, s n := by rw [← hb]; exact sub_lt_self _ (by linarith)
State after:
G : Type
inst✝³ : NormedAddCommGroup G
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : SecondCountableTopology E
s : ℕ → ℝ
ba : BddAbove (range s)
e : ℝ
ep : e > 0
b : ℝ
hb : (⨆ n, s n) - e = b
bs : b < ⨆ n, s n
⊢ ∃ N, ∀ n ≥ N, dist ((partialSups s) n) (⨆ n, s n) < e

State before:
G : Type
inst✝³ : NormedAddCommGroup G
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : SecondCountableTopology E
s : ℕ → ℝ
ba : BddAbove (range s)
e : ℝ
ep : e > 0
b : ℝ
hb : (⨆ n, s n) - e = b
bs : b < ⨆ n, s n
⊢ ∃ N, ∀ n ≥ N, dist ((partialSups s) n) (⨆ n, s n) < e
Tactic:
rcases exists_lt_of_lt_ciSup bs with ⟨N, sN⟩
State after:
case intro
G : Type
inst✝³ : NormedAddCommGroup G
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : SecondCountableTopology E
s : ℕ → ℝ
ba : BddAbove (range s)
e : ℝ
ep : e > 0
b : ℝ
hb : (⨆ n, s n) - e = b
bs : b < ⨆ n, s n
N : ℕ
sN : b < s N
⊢ ∃ N, ∀ n ≥ N, dist ((partialSups s) n) (⨆ n, s n) < e

State before:
case intro
G : Type
inst✝³ : NormedAddCommGroup G
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : SecondCountableTopology E
s : ℕ → ℝ
ba : BddAbove (range s)
e : ℝ
ep : e > 0
b : ℝ
hb : (⨆ n, s n) - e = b
bs : b < ⨆ n, s n
N : ℕ
sN : b < s N
⊢ ∃ N, ∀ n ≥ N, dist ((partialSups s) n) (⨆ n, s n) < e
Tactic:
use N
State after:
case h
G : Type
inst✝³ : NormedAddCommGroup G
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : SecondCountableTopology E
s : ℕ → ℝ
ba : BddAbove (range s)
e : ℝ
ep : e > 0
b : ℝ
hb : (⨆ n, s n) - e = b
bs : b < ⨆ n, s n
N : ℕ
sN : b < s N
⊢ ∀ n ≥ N, dist ((partialSups s) n) (⨆ n, s n) < e

State before:
case h
G : Type
inst✝³ : NormedAddCommGroup G
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : SecondCountableTopology E
s : ℕ → ℝ
ba : BddAbove (range s)
e : ℝ
ep : e > 0
b : ℝ
hb : (⨆ n, s n) - e = b
bs : b < ⨆ n, s n
N : ℕ
sN : b < s N
⊢ ∀ n ≥ N, dist ((partialSups s) n) (⨆ n, s n) < e
Tactic:
intro n nN
State after:
case h
G : Type
inst✝³ : NormedAddCommGroup G
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : SecondCountableTopology E
s : ℕ → ℝ
ba : BddAbove (range s)
e : ℝ
ep : e > 0
b : ℝ
hb : (⨆ n, s n) - e = b
bs : b < ⨆ n, s n
N : ℕ
sN : b < s N
n : ℕ
nN : n ≥ N
⊢ dist ((partialSups s) n) (⨆ n, s n) < e

State before:
case h
G : Type
inst✝³ : NormedAddCommGroup G
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : SecondCountableTopology E
s : ℕ → ℝ
ba : BddAbove (range s)
e : ℝ
ep : e > 0
b : ℝ
hb : (⨆ n, s n) - e = b
bs : b < ⨆ n, s n
N : ℕ
sN : b < s N
n : ℕ
nN : n ≥ N
⊢ dist ((partialSups s) n) (⨆ n, s n) < e
Tactic:
rw [Real.dist_eq]
State after:
case h
G : Type
inst✝³ : NormedAddCommGroup G
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : SecondCountableTopology E
s : ℕ → ℝ
ba : BddAbove (range s)
e : ℝ
ep : e > 0
b : ℝ
hb : (⨆ n, s n) - e = b
bs : b < ⨆ n, s n
N : ℕ
sN : b < s N
n : ℕ
nN : n ≥ N
⊢ |(partialSups s) n - ⨆ n, s n| < e

State before:
case h
G : Type
inst✝³ : NormedAddCommGroup G
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : SecondCountableTopology E
s : ℕ → ℝ
ba : BddAbove (range s)
e : ℝ
ep : e > 0
b : ℝ
hb : (⨆ n, s n) - e = b
bs : b < ⨆ n, s n
N : ℕ
sN : b < s N
n : ℕ
nN : n ≥ N
⊢ |(partialSups s) n - ⨆ n, s n| < e
Tactic:
rw [abs_lt]
State after:
case h
G : Type
inst✝³ : NormedAddCommGroup G
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : SecondCountableTopology E
s : ℕ → ℝ
ba : BddAbove (range s)
e : ℝ
ep : e > 0
b : ℝ
hb : (⨆ n, s n) - e = b
bs : b < ⨆ n, s n
N : ℕ
sN : b < s N
n : ℕ
nN : n ≥ N
⊢ -e < (partialSups s) n - ⨆ n, s n ∧ (partialSups s) n - ⨆ n, s n < e

State before:
case h
G : Type
inst✝³ : NormedAddCommGroup G
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : SecondCountableTopology E
s : ℕ → ℝ
ba : BddAbove (range s)
e : ℝ
ep : e > 0
b : ℝ
hb : (⨆ n, s n) - e = b
bs : b < ⨆ n, s n
N : ℕ
sN : b < s N
n : ℕ
nN : n ≥ N
⊢ -e < (partialSups s) n - ⨆ n, s n ∧ (partialSups s) n - ⨆ n, s n < e
Tactic:
constructor
State after:
case h.left
G : Type
inst✝³ : NormedAddCommGroup G
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : SecondCountableTopology E
s : ℕ → ℝ
ba : BddAbove (range s)
e : ℝ
ep : e > 0
b : ℝ
hb : (⨆ n, s n) - e = b
bs : b < ⨆ n, s n
N : ℕ
sN : b < s N
n : ℕ
nN : n ≥ N
⊢ -e < (partialSups s) n - ⨆ n, s n

case h.right
G : Type
inst✝³ : NormedAddCommGroup G
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : SecondCountableTopology E
s : ℕ → ℝ
ba : BddAbove (range s)
e : ℝ
ep : e > 0
b : ℝ
hb : (⨆ n, s n) - e = b
bs : b < ⨆ n, s n
N : ℕ
sN : b < s N
n : ℕ
nN : n ≥ N
⊢ (partialSups s) n - ⨆ n, s n < e

State before:
G : Type
inst✝³ : NormedAddCommGroup G
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : SecondCountableTopology E
s : ℕ → ℝ
ba : BddAbove (range s)
e : ℝ
ep : e > 0
b : ℝ
hb : (⨆ n, s n) - e = b
⊢ b < ⨆ n, s n
Tactic:
rw [← hb]
State after:
G : Type
inst✝³ : NormedAddCommGroup G
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : SecondCountableTopology E
s : ℕ → ℝ
ba : BddAbove (range s)
e : ℝ
ep : e > 0
b : ℝ
hb : (⨆ n, s n) - e = b
⊢ (⨆ n, s n) - e < ⨆ n, s n

State before:
G : Type
inst✝³ : NormedAddCommGroup G
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : SecondCountableTopology E
s : ℕ → ℝ
ba : BddAbove (range s)
e : ℝ
ep : e > 0
b : ℝ
hb : (⨆ n, s n) - e = b
⊢ (⨆ n, s n) - e < ⨆ n, s n
Tactic:
exact sub_lt_self _ (by linarith)
State after:
no goals

State before:
G : Type
inst✝³ : NormedAddCommGroup G
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : SecondCountableTopology E
s : ℕ → ℝ
ba : BddAbove (range s)
e : ℝ
ep : e > 0
b : ℝ
hb : (⨆ n, s n) - e = b
⊢ 0 < e
Tactic:
linarith
State after:
no goals

State before:
case h.left
G : Type
inst✝³ : NormedAddCommGroup G
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : SecondCountableTopology E
s : ℕ → ℝ
ba : BddAbove (range s)
e : ℝ
ep : e > 0
b : ℝ
hb : (⨆ n, s n) - e = b
bs : b < ⨆ n, s n
N : ℕ
sN : b < s N
n : ℕ
nN : n ≥ N
⊢ -e < (partialSups s) n - ⨆ n, s n
Tactic:
simp only [neg_lt_sub_iff_lt_add]
State after:
case h.left
G : Type
inst✝³ : NormedAddCommGroup G
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : SecondCountableTopology E
s : ℕ → ℝ
ba : BddAbove (range s)
e : ℝ
ep : e > 0
b : ℝ
hb : (⨆ n, s n) - e = b
bs : b < ⨆ n, s n
N : ℕ
sN : b < s N
n : ℕ
nN : n ≥ N
⊢ ⨆ n, s n < e + (partialSups s) n

State before:
case h.left
G : Type
inst✝³ : NormedAddCommGroup G
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : SecondCountableTopology E
s : ℕ → ℝ
ba : BddAbove (range s)
e : ℝ
ep : e > 0
b : ℝ
hb : (⨆ n, s n) - e = b
bs : b < ⨆ n, s n
N : ℕ
sN : b < s N
n : ℕ
nN : n ≥ N
⊢ ⨆ n, s n < e + (partialSups s) n
Tactic:
simp only [←hb] at sN
State after:
case h.left
G : Type
inst✝³ : NormedAddCommGroup G
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : SecondCountableTopology E
s : ℕ → ℝ
ba : BddAbove (range s)
e : ℝ
ep : e > 0
b : ℝ
hb : (⨆ n, s n) - e = b
bs : b < ⨆ n, s n
N n : ℕ
nN : n ≥ N
sN : (⨆ n, s n) - e < s N
⊢ ⨆ n, s n < e + (partialSups s) n

State before:
case h.left
G : Type
inst✝³ : NormedAddCommGroup G
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : SecondCountableTopology E
s : ℕ → ℝ
ba : BddAbove (range s)
e : ℝ
ep : e > 0
b : ℝ
hb : (⨆ n, s n) - e = b
bs : b < ⨆ n, s n
N n : ℕ
nN : n ≥ N
sN : (⨆ n, s n) - e < s N
⊢ ⨆ n, s n < e + (partialSups s) n
Tactic:
calc iSup s
  _ = iSup s - e + e := by ring
  _ < s N + e := by linarith
  _ ≤ partialSups s n + e := by linarith [le_partialSups_of_le s nN]
  _ = e + partialSups s n := by ring
State after:
no goals

State before:
G : Type
inst✝³ : NormedAddCommGroup G
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : SecondCountableTopology E
s : ℕ → ℝ
ba : BddAbove (range s)
e : ℝ
ep : e > 0
b : ℝ
hb : (⨆ n, s n) - e = b
bs : b < ⨆ n, s n
N n : ℕ
nN : n ≥ N
sN : (⨆ n, s n) - e < s N
⊢ iSup s = iSup s - e + e
Tactic:
ring
State after:
no goals

State before:
G : Type
inst✝³ : NormedAddCommGroup G
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : SecondCountableTopology E
s : ℕ → ℝ
ba : BddAbove (range s)
e : ℝ
ep : e > 0
b : ℝ
hb : (⨆ n, s n) - e = b
bs : b < ⨆ n, s n
N n : ℕ
nN : n ≥ N
sN : (⨆ n, s n) - e < s N
⊢ iSup s - e + e < s N + e
Tactic:
linarith
State after:
no goals

State before:
G : Type
inst✝³ : NormedAddCommGroup G
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : SecondCountableTopology E
s : ℕ → ℝ
ba : BddAbove (range s)
e : ℝ
ep : e > 0
b : ℝ
hb : (⨆ n, s n) - e = b
bs : b < ⨆ n, s n
N n : ℕ
nN : n ≥ N
sN : (⨆ n, s n) - e < s N
⊢ s N + e ≤ (partialSups s) n + e
Tactic:
linarith [le_partialSups_of_le s nN]
State after:
no goals

State before:
G : Type
inst✝³ : NormedAddCommGroup G
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : SecondCountableTopology E
s : ℕ → ℝ
ba : BddAbove (range s)
e : ℝ
ep : e > 0
b : ℝ
hb : (⨆ n, s n) - e = b
bs : b < ⨆ n, s n
N n : ℕ
nN : n ≥ N
sN : (⨆ n, s n) - e < s N
⊢ (partialSups s) n + e = e + (partialSups s) n
Tactic:
ring
State after:
no goals

State before:
case h.right
G : Type
inst✝³ : NormedAddCommGroup G
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : SecondCountableTopology E
s : ℕ → ℝ
ba : BddAbove (range s)
e : ℝ
ep : e > 0
b : ℝ
hb : (⨆ n, s n) - e = b
bs : b < ⨆ n, s n
N : ℕ
sN : b < s N
n : ℕ
nN : n ≥ N
⊢ (partialSups s) n - ⨆ n, s n < e
Tactic:
have rs : partialSups s n ≤ iSup s := partialSups_le _ _ _ fun a _ ↦ le_ciSup ba a
State after:
case h.right
G : Type
inst✝³ : NormedAddCommGroup G
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : SecondCountableTopology E
s : ℕ → ℝ
ba : BddAbove (range s)
e : ℝ
ep : e > 0
b : ℝ
hb : (⨆ n, s n) - e = b
bs : b < ⨆ n, s n
N : ℕ
sN : b < s N
n : ℕ
nN : n ≥ N
rs : (partialSups s) n ≤ iSup s
⊢ (partialSups s) n - ⨆ n, s n < e

State before:
case h.right
G : Type
inst✝³ : NormedAddCommGroup G
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : SecondCountableTopology E
s : ℕ → ℝ
ba : BddAbove (range s)
e : ℝ
ep : e > 0
b : ℝ
hb : (⨆ n, s n) - e = b
bs : b < ⨆ n, s n
N : ℕ
sN : b < s N
n : ℕ
nN : n ≥ N
rs : (partialSups s) n ≤ iSup s
⊢ (partialSups s) n - ⨆ n, s n < e
Tactic:
calc partialSups s n - iSup s
  _ ≤ iSup s - iSup s := by linarith
  _ = 0 := by ring
  _ < e := ep
State after:
no goals

State before:
G : Type
inst✝³ : NormedAddCommGroup G
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : SecondCountableTopology E
s : ℕ → ℝ
ba : BddAbove (range s)
e : ℝ
ep : e > 0
b : ℝ
hb : (⨆ n, s n) - e = b
bs : b < ⨆ n, s n
N : ℕ
sN : b < s N
n : ℕ
nN : n ≥ N
rs : (partialSups s) n ≤ iSup s
⊢ (partialSups s) n - iSup s ≤ iSup s - iSup s
Tactic:
linarith
State after:
no goals

State before:
G : Type
inst✝³ : NormedAddCommGroup G
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : SecondCountableTopology E
s : ℕ → ℝ
ba : BddAbove (range s)
e : ℝ
ep : e > 0
b : ℝ
hb : (⨆ n, s n) - e = b
bs : b < ⨆ n, s n
N : ℕ
sN : b < s N
n : ℕ
nN : n ≥ N
rs : (partialSups s) n ≤ iSup s
⊢ iSup s - iSup s = 0
Tactic:
ring
State after:
no goals