α : Type ?u.107946
β : Type ?u.107949
γ : Type ?u.107952
a b c d : ℝ≥0∞
r p q : ℝ≥0
x y z ε ε₁ ε₂ : ℝ≥0∞
s : Set ℝ≥0∞
⊢ ∀ (x : ℝ≥0∞ × ℝ≥0∞), x ∈ {p | p ≠ (⊤, ⊤)} → ContinuousWithinAt (fun p => p.fst - p.snd) {p | p ≠ (⊤, ⊤)} x
α : Type ?u.107946
β : Type ?u.107949
γ : Type ?u.107952
a b c d : ℝ≥0∞
r p q : ℝ≥0
x y z ε ε₁ ε₂ : ℝ≥0∞
s : Set ℝ≥0∞
⊢ ContinuousOn (fun p => p.fst - p.snd) {p | p ≠ (⊤, ⊤)}
rw [ContinuousOn]
case mk
α : Type ?u.107946
β : Type ?u.107949
γ : Type ?u.107952
a b c d : ℝ≥0∞
r p q : ℝ≥0
x✝ y✝ z ε ε₁ ε₂ : ℝ≥0∞
s : Set ℝ≥0∞
x y : ℝ≥0∞
hp : (x, y) ∈ {p | p ≠ (⊤, ⊤)}
⊢ ContinuousWithinAt (fun p => p.fst - p.snd) {p | p ≠ (⊤, ⊤)} (x, y)
α : Type ?u.107946
β : Type ?u.107949
γ : Type ?u.107952
a b c d : ℝ≥0∞
r p q : ℝ≥0
x y z ε ε₁ ε₂ : ℝ≥0∞
s : Set ℝ≥0∞
⊢ ∀ (x : ℝ≥0∞ × ℝ≥0∞), x ∈ {p | p ≠ (⊤, ⊤)} → ContinuousWithinAt (fun p => p.fst - p.snd) {p | p ≠ (⊤, ⊤)} x
rintro ⟨x, y⟩ hp
case mk
α : Type ?u.107946
β : Type ?u.107949
γ : Type ?u.107952
a b c d : ℝ≥0∞
r p q : ℝ≥0
x✝ y✝ z ε ε₁ ε₂ : ℝ≥0∞
s : Set ℝ≥0∞
x y : ℝ≥0∞
hp : ¬(x = ⊤ ∧ y = ⊤)
⊢ ContinuousWithinAt (fun p => p.fst - p.snd) {p | p ≠ (⊤, ⊤)} (x, y)
case mk
α : Type ?u.107946
β : Type ?u.107949
γ : Type ?u.107952
a b c d : ℝ≥0∞
r p q : ℝ≥0
x✝ y✝ z ε ε₁ ε₂ : ℝ≥0∞
s : Set ℝ≥0∞
x y : ℝ≥0∞
hp : (x, y) ∈ {p | p ≠ (⊤, ⊤)}
⊢ ContinuousWithinAt (fun p => p.fst - p.snd) {p | p ≠ (⊤, ⊤)} (x, y)
simp only [Ne.def, Set.mem_setOf_eq, Prod.mk.inj_iff] at hp
no goals
case mk
α : Type ?u.107946
β : Type ?u.107949
γ : Type ?u.107952
a b c d : ℝ≥0∞
r p q : ℝ≥0
x✝ y✝ z ε ε₁ ε₂ : ℝ≥0∞
s : Set ℝ≥0∞
x y : ℝ≥0∞
hp : ¬(x = ⊤ ∧ y = ⊤)
⊢ ContinuousWithinAt (fun p => p.fst - p.snd) {p | p ≠ (⊤, ⊤)} (x, y)
refine' tendsto_nhdsWithin_of_tendsto_nhds (tendsto_sub (not_and_or.mp hp))