no goals
α : Type ?u.83081
β : Type ?u.83084
γ : Type ?u.83087
a b c d : ℝ≥0∞
r p q : ℝ≥0
x y z ε ε₁ ε₂ : ℝ≥0∞
s : Set ℝ≥0∞
h : ⊤ ≠ ⊤ ∨ ⊤ ≠ ⊤
⊢ Tendsto (fun p => p.fst - p.snd) (𝓝 (⊤, ⊤)) (𝓝 (⊤ - ⊤))
simp only at h
α : Type ?u.83081
β : Type ?u.83084
γ : Type ?u.83087
a b✝ c d : ℝ≥0∞
r p q : ℝ≥0
x y z ε ε₁ ε₂ : ℝ≥0∞
s : Set ℝ≥0∞
b : ℝ≥0
x✝ : ⊤ ≠ ⊤ ∨ ↑b ≠ ⊤
⊢ ∀ (x : ℝ≥0), ∀ᶠ (a : ℝ≥0∞ × ℝ≥0∞) in 𝓝 (⊤, ↑b), ↑x < a.fst - a.snd
α : Type ?u.83081
β : Type ?u.83084
γ : Type ?u.83087
a b✝ c d : ℝ≥0∞
r p q : ℝ≥0
x y z ε ε₁ ε₂ : ℝ≥0∞
s : Set ℝ≥0∞
b : ℝ≥0
x✝ : ⊤ ≠ ⊤ ∨ ↑b ≠ ⊤
⊢ Tendsto (fun p => p.fst - p.snd) (𝓝 (⊤, ↑b)) (𝓝 (⊤ - ↑b))
rw [top_sub_coe, tendsto_nhds_top_iff_nnreal]
α : Type ?u.83081
β : Type ?u.83084
γ : Type ?u.83087
a b✝ c d : ℝ≥0∞
r p q : ℝ≥0
x✝¹ y✝ z ε ε₁ ε₂ : ℝ≥0∞
s : Set ℝ≥0∞
b : ℝ≥0
x✝ : ⊤ ≠ ⊤ ∨ ↑b ≠ ⊤
x : ℝ≥0
y : ℝ≥0∞ × ℝ≥0∞
hy : ↑(b + 1 + x) < y.fst ∧ y.snd ≤ ↑(b + 1)
⊢ ↑x < y.fst - y.snd
α : Type ?u.83081
β : Type ?u.83084
γ : Type ?u.83087
a b✝ c d : ℝ≥0∞
r p q : ℝ≥0
x y z ε ε₁ ε₂ : ℝ≥0∞
s : Set ℝ≥0∞
b : ℝ≥0
x✝ : ⊤ ≠ ⊤ ∨ ↑b ≠ ⊤
⊢ ∀ (x : ℝ≥0), ∀ᶠ (a : ℝ≥0∞ × ℝ≥0∞) in 𝓝 (⊤, ↑b), ↑x < a.fst - a.snd
refine fun x => ((lt_mem_nhds <| @coe_lt_top (b + 1 + x)).prod_nhds
  (ge_mem_nhds <| coe_lt_coe.2 <| lt_add_one b)).mono fun y hy => ?_
α : Type ?u.83081
β : Type ?u.83084
γ : Type ?u.83087
a b✝ c d : ℝ≥0∞
r p q : ℝ≥0
x✝¹ y✝ z ε ε₁ ε₂ : ℝ≥0∞
s : Set ℝ≥0∞
b : ℝ≥0
x✝ : ⊤ ≠ ⊤ ∨ ↑b ≠ ⊤
x : ℝ≥0
y : ℝ≥0∞ × ℝ≥0∞
hy : ↑(b + 1 + x) < y.fst ∧ y.snd ≤ ↑(b + 1)
⊢ y.snd + ↑x < y.fst
α : Type ?u.83081
β : Type ?u.83084
γ : Type ?u.83087
a b✝ c d : ℝ≥0∞
r p q : ℝ≥0
x✝¹ y✝ z ε ε₁ ε₂ : ℝ≥0∞
s : Set ℝ≥0∞
b : ℝ≥0
x✝ : ⊤ ≠ ⊤ ∨ ↑b ≠ ⊤
x : ℝ≥0
y : ℝ≥0∞ × ℝ≥0∞
hy : ↑(b + 1 + x) < y.fst ∧ y.snd ≤ ↑(b + 1)
⊢ ↑x < y.fst - y.snd
rw [lt_tsub_iff_left]
no goals
α : Type ?u.83081
β : Type ?u.83084
γ : Type ?u.83087
a b✝ c d : ℝ≥0∞
r p q : ℝ≥0
x✝¹ y✝ z ε ε₁ ε₂ : ℝ≥0∞
s : Set ℝ≥0∞
b : ℝ≥0
x✝ : ⊤ ≠ ⊤ ∨ ↑b ≠ ⊤
x : ℝ≥0
y : ℝ≥0∞ × ℝ≥0∞
hy : ↑(b + 1 + x) < y.fst ∧ y.snd ≤ ↑(b + 1)
⊢ y.snd + ↑x < y.fst
calc y.2 + x ≤ ↑(b + 1) + x := add_le_add_right hy.2 _
_ < y.1 := hy.1
α : Type ?u.83081
β : Type ?u.83084
γ : Type ?u.83087
a✝ b c d : ℝ≥0∞
r p q : ℝ≥0
x y z ε ε₁ ε₂ : ℝ≥0∞
s : Set ℝ≥0∞
a : ℝ≥0
x✝ : ↑a ≠ ⊤ ∨ ⊤ ≠ ⊤
⊢ Tendsto (fun p => p.fst - p.snd) (𝓝 (↑a, ⊤)) (𝓝 0)
α : Type ?u.83081
β : Type ?u.83084
γ : Type ?u.83087
a✝ b c d : ℝ≥0∞
r p q : ℝ≥0
x y z ε ε₁ ε₂ : ℝ≥0∞
s : Set ℝ≥0∞
a : ℝ≥0
x✝ : ↑a ≠ ⊤ ∨ ⊤ ≠ ⊤
⊢ Tendsto (fun p => p.fst - p.snd) (𝓝 (↑a, ⊤)) (𝓝 (↑a - ⊤))
rw [sub_top]
α : Type ?u.83081
β : Type ?u.83084
γ : Type ?u.83087
a✝ b c d : ℝ≥0∞
r p q : ℝ≥0
x y z ε ε₁ ε₂ : ℝ≥0∞
s : Set ℝ≥0∞
a : ℝ≥0
x✝ : ↑a ≠ ⊤ ∨ ⊤ ≠ ⊤
⊢ ∀ᶠ (x : ℝ≥0∞ × ℝ≥0∞) in 𝓝 (↑a, ⊤), x.fst - x.snd = 0
α : Type ?u.83081
β : Type ?u.83084
γ : Type ?u.83087
a✝ b c d : ℝ≥0∞
r p q : ℝ≥0
x y z ε ε₁ ε₂ : ℝ≥0∞
s : Set ℝ≥0∞
a : ℝ≥0
x✝ : ↑a ≠ ⊤ ∨ ⊤ ≠ ⊤
⊢ Tendsto (fun p => p.fst - p.snd) (𝓝 (↑a, ⊤)) (𝓝 0)
refine (tendsto_pure.2 ?_).mono_right (pure_le_nhds _)
no goals
α : Type ?u.83081
β : Type ?u.83084
γ : Type ?u.83087
a✝ b c d : ℝ≥0∞
r p q : ℝ≥0
x y z ε ε₁ ε₂ : ℝ≥0∞
s : Set ℝ≥0∞
a : ℝ≥0
x✝ : ↑a ≠ ⊤ ∨ ⊤ ≠ ⊤
⊢ ∀ᶠ (x : ℝ≥0∞ × ℝ≥0∞) in 𝓝 (↑a, ⊤), x.fst - x.snd = 0
exact ((gt_mem_nhds <| coe_lt_coe.2 <| lt_add_one a).prod_nhds
  (lt_mem_nhds <| @coe_lt_top (a + 1))).mono fun x hx =>
    tsub_eq_zero_iff_le.2 (hx.1.trans hx.2).le
no goals
α : Type ?u.83081
β : Type ?u.83084
γ : Type ?u.83087
a✝ b✝ c d : ℝ≥0∞
r p q : ℝ≥0
x y z ε ε₁ ε₂ : ℝ≥0∞
s : Set ℝ≥0∞
a b : ℝ≥0
x✝ : ↑a ≠ ⊤ ∨ ↑b ≠ ⊤
⊢ Tendsto (fun a => a.fst - a.snd) (𝓝 (a, b)) (𝓝 (a - b))
exact continuous_sub.tendsto (a, b)