[GOAL]
α : Type u_1
inst✝ : TopologicalSpace α
⊢ OrdConnected (range Real.toEReal)
[PROOFSTEP]
rw [range_coe_eq_Ioo]
[GOAL]
α : Type u_1
inst✝ : TopologicalSpace α
⊢ OrdConnected (Ioo ⊥ ⊤)
[PROOFSTEP]
exact ordConnected_Ioo
[GOAL]
α : Type u_1
inst✝ : TopologicalSpace α
⊢ IsOpen (range Real.toEReal)
[PROOFSTEP]
simp only [range_coe_eq_Ioo, isOpen_Ioo]
[GOAL]
α : Type u_1
inst✝ : TopologicalSpace α
a : EReal
ha : a ≠ ⊤
h'a : a ≠ ⊥
⊢ Tendsto toReal (𝓝 a) (𝓝 (toReal a))
[PROOFSTEP]
lift a to ℝ using ⟨ha, h'a⟩
[GOAL]
case intro
α : Type u_1
inst✝ : TopologicalSpace α
a : ℝ
ha : ↑a ≠ ⊤
h'a : ↑a ≠ ⊥
⊢ Tendsto toReal (𝓝 ↑a) (𝓝 (toReal ↑a))
[PROOFSTEP]
rw [nhds_coe, tendsto_map'_iff]
[GOAL]
case intro
α : Type u_1
inst✝ : TopologicalSpace α
a : ℝ
ha : ↑a ≠ ⊤
h'a : ↑a ≠ ⊥
⊢ Tendsto (toReal ∘ Real.toEReal) (𝓝 a) (𝓝 (toReal ↑a))
[PROOFSTEP]
exact tendsto_id
[GOAL]
α : Type u_1
inst✝ : TopologicalSpace α
⊢ OrdConnected (range ENNReal.toEReal)
[PROOFSTEP]
rw [range_coe_ennreal]
[GOAL]
α : Type u_1
inst✝ : TopologicalSpace α
⊢ OrdConnected (Ici 0)
[PROOFSTEP]
exact ordConnected_Ici
[GOAL]
α : Type u_1
inst✝ : TopologicalSpace α
⊢ IsClosed (range ENNReal.toEReal)
[PROOFSTEP]
rw [range_coe_ennreal]
[GOAL]
α : Type u_1
inst✝ : TopologicalSpace α
⊢ IsClosed (Ici 0)
[PROOFSTEP]
exact isClosed_Ici
[GOAL]
α : Type u_1
inst✝ : TopologicalSpace α
⊢ ⨅ (l : EReal) (_ : l < ⊤), 𝓟 (Ioi l) = ⨅ (a : EReal) (_ : a ≠ ⊤), 𝓟 (Ioi a)
[PROOFSTEP]
simp only [lt_top_iff_ne_top]
[GOAL]
α : Type u_1
inst✝ : TopologicalSpace α
⊢ HasBasis (𝓝 ⊤) (fun x => True) fun x => Ioi ↑x
[PROOFSTEP]
refine nhds_top_basis.to_hasBasis (fun x hx => ?_) fun _ _ ↦ ⟨_, coe_lt_top _, Subset.rfl⟩
[GOAL]
α : Type u_1
inst✝ : TopologicalSpace α
x : EReal
hx : x < ⊤
⊢ ∃ i', True ∧ Ioi ↑i' ⊆ Ioi x
[PROOFSTEP]
rcases exists_rat_btwn_of_lt hx with ⟨y, hxy, -⟩
[GOAL]
case intro.intro
α : Type u_1
inst✝ : TopologicalSpace α
x : EReal
hx : x < ⊤
y : ℚ
hxy : x < ↑↑y
⊢ ∃ i', True ∧ Ioi ↑i' ⊆ Ioi x
[PROOFSTEP]
exact ⟨_, trivial, Ioi_subset_Ioi hxy.le⟩
[GOAL]
α : Type u_1
inst✝ : TopologicalSpace α
s : Set EReal
⊢ (∃ i, True ∧ Ioi ↑i ⊆ s) ↔ ∃ y, Ioi ↑y ⊆ s
[PROOFSTEP]
simp only [true_and]
[GOAL]
α✝ : Type u_1
inst✝ : TopologicalSpace α✝
α : Type u_2
m : α → EReal
f : Filter α
⊢ (∀ (i : ℝ), True → ∀ᶠ (x : α) in f, m x ∈ Ioi ↑i) ↔ ∀ (x : ℝ), ∀ᶠ (a : α) in f, ↑x < m a
[PROOFSTEP]
simp only [true_implies, mem_Ioi]
[GOAL]
α : Type u_1
inst✝ : TopologicalSpace α
⊢ ⨅ (l : EReal) (_ : ⊥ < l), 𝓟 (Iio l) = ⨅ (a : EReal) (_ : a ≠ ⊥), 𝓟 (Iio a)
[PROOFSTEP]
simp only [bot_lt_iff_ne_bot]
[GOAL]
α : Type u_1
inst✝ : TopologicalSpace α
⊢ HasBasis (𝓝 ⊥) (fun x => True) fun x => Iio ↑x
[PROOFSTEP]
refine nhds_bot_basis.to_hasBasis (fun x hx => ?_) fun _ _ ↦ ⟨_, bot_lt_coe _, Subset.rfl⟩
[GOAL]
α : Type u_1
inst✝ : TopologicalSpace α
x : EReal
hx : ⊥ < x
⊢ ∃ i', True ∧ Iio ↑i' ⊆ Iio x
[PROOFSTEP]
rcases exists_rat_btwn_of_lt hx with ⟨y, -, hxy⟩
[GOAL]
case intro.intro
α : Type u_1
inst✝ : TopologicalSpace α
x : EReal
hx : ⊥ < x
y : ℚ
hxy : ↑↑y < x
⊢ ∃ i', True ∧ Iio ↑i' ⊆ Iio x
[PROOFSTEP]
exact ⟨_, trivial, Iio_subset_Iio hxy.le⟩
[GOAL]
α : Type u_1
inst✝ : TopologicalSpace α
s : Set EReal
⊢ (∃ i, True ∧ Iio ↑i ⊆ s) ↔ ∃ y, Iio ↑y ⊆ s
[PROOFSTEP]
simp only [true_and]
[GOAL]
α✝ : Type u_1
inst✝ : TopologicalSpace α✝
α : Type u_2
m : α → EReal
f : Filter α
⊢ (∀ (i : ℝ), True → ∀ᶠ (x : α) in f, m x ∈ Iio ↑i) ↔ ∀ (x : ℝ), ∀ᶠ (a : α) in f, m a < ↑x
[PROOFSTEP]
simp only [true_implies, mem_Iio]
[GOAL]
α : Type u_1
inst✝ : TopologicalSpace α
a b : ℝ
⊢ ContinuousAt (fun p => p.fst + p.snd) (↑a, ↑b)
[PROOFSTEP]
simp only [ContinuousAt, nhds_coe_coe, ← coe_add, tendsto_map'_iff, (· ∘ ·), tendsto_coe, tendsto_add]
[GOAL]
α : Type u_1
inst✝ : TopologicalSpace α
a : ℝ
⊢ ContinuousAt (fun p => p.fst + p.snd) (⊤, ↑a)
[PROOFSTEP]
simp only [ContinuousAt, tendsto_nhds_top_iff_real, top_add_coe]
[GOAL]
α : Type u_1
inst✝ : TopologicalSpace α
a : ℝ
⊢ ∀ (x : ℝ), ∀ᶠ (a : EReal × EReal) in 𝓝 (⊤, ↑a), ↑x < a.fst + a.snd
[PROOFSTEP]
refine fun r ↦
  ((lt_mem_nhds (coe_lt_top (r - (a - 1)))).prod_nhds (lt_mem_nhds <| EReal.coe_lt_coe_iff.2 <| sub_one_lt _)).mono
    fun _ h ↦ ?_
[GOAL]
α : Type u_1
inst✝ : TopologicalSpace α
a r : ℝ
x✝ : EReal × EReal
h : ↑(r - (a - 1)) < x✝.fst ∧ ↑(a - 1) < x✝.snd
⊢ ↑r < x✝.fst + x✝.snd
[PROOFSTEP]
simpa only [← coe_add, sub_add_cancel] using add_lt_add h.1 h.2
[GOAL]
α : Type u_1
inst✝ : TopologicalSpace α
a : ℝ
⊢ ContinuousAt (fun p => p.fst + p.snd) (↑a, ⊤)
[PROOFSTEP]
simpa only [add_comm, (· ∘ ·), ContinuousAt, Prod.swap] using
  Tendsto.comp (continuousAt_add_top_coe a) (continuous_swap.tendsto ((a : EReal), ⊤))
[GOAL]
α : Type u_1
inst✝ : TopologicalSpace α
⊢ ContinuousAt (fun p => p.fst + p.snd) (⊤, ⊤)
[PROOFSTEP]
simp only [ContinuousAt, tendsto_nhds_top_iff_real, top_add_top]
[GOAL]
α : Type u_1
inst✝ : TopologicalSpace α
⊢ ∀ (x : ℝ), ∀ᶠ (a : EReal × EReal) in 𝓝 (⊤, ⊤), ↑x < a.fst + a.snd
[PROOFSTEP]
refine fun r ↦ ((lt_mem_nhds (coe_lt_top 0)).prod_nhds (lt_mem_nhds <| coe_lt_top r)).mono fun _ h ↦ ?_
[GOAL]
α : Type u_1
inst✝ : TopologicalSpace α
r : ℝ
x✝ : EReal × EReal
h : ↑0 < x✝.fst ∧ ↑r < x✝.snd
⊢ ↑r < x✝.fst + x✝.snd
[PROOFSTEP]
simpa only [coe_zero, zero_add] using add_lt_add h.1 h.2
[GOAL]
α : Type u_1
inst✝ : TopologicalSpace α
a : ℝ
⊢ ContinuousAt (fun p => p.fst + p.snd) (⊥, ↑a)
[PROOFSTEP]
simp only [ContinuousAt, tendsto_nhds_bot_iff_real, bot_add]
[GOAL]
α : Type u_1
inst✝ : TopologicalSpace α
a : ℝ
⊢ ∀ (x : ℝ), ∀ᶠ (a : EReal × EReal) in 𝓝 (⊥, ↑a), a.fst + a.snd < ↑x
[PROOFSTEP]
refine fun r ↦
  ((gt_mem_nhds (bot_lt_coe (r - (a + 1)))).prod_nhds (gt_mem_nhds <| EReal.coe_lt_coe_iff.2 <| lt_add_one _)).mono
    fun _ h ↦ ?_
[GOAL]
α : Type u_1
inst✝ : TopologicalSpace α
a r : ℝ
x✝ : EReal × EReal
h : x✝.fst < ↑(r - (a + 1)) ∧ x✝.snd < ↑(a + 1)
⊢ x✝.fst + x✝.snd < ↑r
[PROOFSTEP]
simpa only [← coe_add, sub_add_cancel] using add_lt_add h.1 h.2
[GOAL]
α : Type u_1
inst✝ : TopologicalSpace α
a : ℝ
⊢ ContinuousAt (fun p => p.fst + p.snd) (↑a, ⊥)
[PROOFSTEP]
simpa only [add_comm, (· ∘ ·), ContinuousAt, Prod.swap] using
  Tendsto.comp (continuousAt_add_bot_coe a) (continuous_swap.tendsto ((a : EReal), ⊥))
[GOAL]
α : Type u_1
inst✝ : TopologicalSpace α
⊢ ContinuousAt (fun p => p.fst + p.snd) (⊥, ⊥)
[PROOFSTEP]
simp only [ContinuousAt, tendsto_nhds_bot_iff_real, bot_add]
[GOAL]
α : Type u_1
inst✝ : TopologicalSpace α
⊢ ∀ (x : ℝ), ∀ᶠ (a : EReal × EReal) in 𝓝 (⊥, ⊥), a.fst + a.snd < ↑x
[PROOFSTEP]
refine fun r ↦ ((gt_mem_nhds (bot_lt_coe 0)).prod_nhds (gt_mem_nhds <| bot_lt_coe r)).mono fun _ h ↦ ?_
[GOAL]
α : Type u_1
inst✝ : TopologicalSpace α
r : ℝ
x✝ : EReal × EReal
h : x✝.fst < ↑0 ∧ x✝.snd < ↑r
⊢ x✝.fst + x✝.snd < ↑r
[PROOFSTEP]
simpa only [coe_zero, zero_add] using add_lt_add h.1 h.2
[GOAL]
α : Type u_1
inst✝ : TopologicalSpace α
p : EReal × EReal
h : p.fst ≠ ⊤ ∨ p.snd ≠ ⊥
h' : p.fst ≠ ⊥ ∨ p.snd ≠ ⊤
⊢ ContinuousAt (fun p => p.fst + p.snd) p
[PROOFSTEP]
rcases p with ⟨x, y⟩
[GOAL]
case mk
α : Type u_1
inst✝ : TopologicalSpace α
x y : EReal
h : (x, y).fst ≠ ⊤ ∨ (x, y).snd ≠ ⊥
h' : (x, y).fst ≠ ⊥ ∨ (x, y).snd ≠ ⊤
⊢ ContinuousAt (fun p => p.fst + p.snd) (x, y)
[PROOFSTEP]
induction x using EReal.rec
[GOAL]
case mk.h_bot
α : Type u_1
inst✝ : TopologicalSpace α
y : EReal
h : (⊥, y).fst ≠ ⊤ ∨ (⊥, y).snd ≠ ⊥
h' : (⊥, y).fst ≠ ⊥ ∨ (⊥, y).snd ≠ ⊤
⊢ ContinuousAt (fun p => p.fst + p.snd) (⊥, y)
[PROOFSTEP]
induction y using EReal.rec
[GOAL]
case mk.h_real
α : Type u_1
inst✝ : TopologicalSpace α
y : EReal
a✝ : ℝ
h : (↑a✝, y).fst ≠ ⊤ ∨ (↑a✝, y).snd ≠ ⊥
h' : (↑a✝, y).fst ≠ ⊥ ∨ (↑a✝, y).snd ≠ ⊤
⊢ ContinuousAt (fun p => p.fst + p.snd) (↑a✝, y)
[PROOFSTEP]
induction y using EReal.rec
[GOAL]
case mk.h_top
α : Type u_1
inst✝ : TopologicalSpace α
y : EReal
h : (⊤, y).fst ≠ ⊤ ∨ (⊤, y).snd ≠ ⊥
h' : (⊤, y).fst ≠ ⊥ ∨ (⊤, y).snd ≠ ⊤
⊢ ContinuousAt (fun p => p.fst + p.snd) (⊤, y)
[PROOFSTEP]
induction y using EReal.rec
[GOAL]
case mk.h_bot.h_bot
α : Type u_1
inst✝ : TopologicalSpace α
h : (⊥, ⊥).fst ≠ ⊤ ∨ (⊥, ⊥).snd ≠ ⊥
h' : (⊥, ⊥).fst ≠ ⊥ ∨ (⊥, ⊥).snd ≠ ⊤
⊢ ContinuousAt (fun p => p.fst + p.snd) (⊥, ⊥)
[PROOFSTEP]
exact continuousAt_add_bot_bot
[GOAL]
case mk.h_bot.h_real
α : Type u_1
inst✝ : TopologicalSpace α
a✝ : ℝ
h : (⊥, ↑a✝).fst ≠ ⊤ ∨ (⊥, ↑a✝).snd ≠ ⊥
h' : (⊥, ↑a✝).fst ≠ ⊥ ∨ (⊥, ↑a✝).snd ≠ ⊤
⊢ ContinuousAt (fun p => p.fst + p.snd) (⊥, ↑a✝)
[PROOFSTEP]
exact continuousAt_add_bot_coe _
[GOAL]
case mk.h_bot.h_top
α : Type u_1
inst✝ : TopologicalSpace α
h : (⊥, ⊤).fst ≠ ⊤ ∨ (⊥, ⊤).snd ≠ ⊥
h' : (⊥, ⊤).fst ≠ ⊥ ∨ (⊥, ⊤).snd ≠ ⊤
⊢ ContinuousAt (fun p => p.fst + p.snd) (⊥, ⊤)
[PROOFSTEP]
simp at h' 
[GOAL]
case mk.h_real.h_bot
α : Type u_1
inst✝ : TopologicalSpace α
a✝ : ℝ
h : (↑a✝, ⊥).fst ≠ ⊤ ∨ (↑a✝, ⊥).snd ≠ ⊥
h' : (↑a✝, ⊥).fst ≠ ⊥ ∨ (↑a✝, ⊥).snd ≠ ⊤
⊢ ContinuousAt (fun p => p.fst + p.snd) (↑a✝, ⊥)
[PROOFSTEP]
exact continuousAt_add_coe_bot _
[GOAL]
case mk.h_real.h_real
α : Type u_1
inst✝ : TopologicalSpace α
a✝¹ a✝ : ℝ
h : (↑a✝¹, ↑a✝).fst ≠ ⊤ ∨ (↑a✝¹, ↑a✝).snd ≠ ⊥
h' : (↑a✝¹, ↑a✝).fst ≠ ⊥ ∨ (↑a✝¹, ↑a✝).snd ≠ ⊤
⊢ ContinuousAt (fun p => p.fst + p.snd) (↑a✝¹, ↑a✝)
[PROOFSTEP]
exact continuousAt_add_coe_coe _ _
[GOAL]
case mk.h_real.h_top
α : Type u_1
inst✝ : TopologicalSpace α
a✝ : ℝ
h : (↑a✝, ⊤).fst ≠ ⊤ ∨ (↑a✝, ⊤).snd ≠ ⊥
h' : (↑a✝, ⊤).fst ≠ ⊥ ∨ (↑a✝, ⊤).snd ≠ ⊤
⊢ ContinuousAt (fun p => p.fst + p.snd) (↑a✝, ⊤)
[PROOFSTEP]
exact continuousAt_add_coe_top _
[GOAL]
case mk.h_top.h_bot
α : Type u_1
inst✝ : TopologicalSpace α
h : (⊤, ⊥).fst ≠ ⊤ ∨ (⊤, ⊥).snd ≠ ⊥
h' : (⊤, ⊥).fst ≠ ⊥ ∨ (⊤, ⊥).snd ≠ ⊤
⊢ ContinuousAt (fun p => p.fst + p.snd) (⊤, ⊥)
[PROOFSTEP]
simp at h 
[GOAL]
case mk.h_top.h_real
α : Type u_1
inst✝ : TopologicalSpace α
a✝ : ℝ
h : (⊤, ↑a✝).fst ≠ ⊤ ∨ (⊤, ↑a✝).snd ≠ ⊥
h' : (⊤, ↑a✝).fst ≠ ⊥ ∨ (⊤, ↑a✝).snd ≠ ⊤
⊢ ContinuousAt (fun p => p.fst + p.snd) (⊤, ↑a✝)
[PROOFSTEP]
exact continuousAt_add_top_coe _
[GOAL]
case mk.h_top.h_top
α : Type u_1
inst✝ : TopologicalSpace α
h : (⊤, ⊤).fst ≠ ⊤ ∨ (⊤, ⊤).snd ≠ ⊥
h' : (⊤, ⊤).fst ≠ ⊥ ∨ (⊤, ⊤).snd ≠ ⊤
⊢ ContinuousAt (fun p => p.fst + p.snd) (⊤, ⊤)
[PROOFSTEP]
exact continuousAt_add_top_top
