α : Type u_1
β : Type ?u.419875
γ : Type ?u.419878
inst✝ : PseudoEMetricSpace α
f : α → ℝ≥0∞
C : ℝ≥0∞
hC : C ≠ ⊤
h : ∀ (x y : α), f x ≤ f y + C * edist x y
x : α
ε : ℝ≥0∞
ε0 : ε > 0
⊢ ∀ᶠ (x_1 : α) in 𝓝 x, f x_1 ∈ Icc (f x - ε) (f x + ε)
α : Type u_1
β : Type ?u.419875
γ : Type ?u.419878
inst✝ : PseudoEMetricSpace α
f : α → ℝ≥0∞
C : ℝ≥0∞
hC : C ≠ ⊤
h : ∀ (x y : α), f x ≤ f y + C * edist x y
⊢ Continuous f
refine continuous_iff_continuousAt.2 fun x => ENNReal.tendsto_nhds_of_Icc fun ε ε0 => ?_
case intro.intro
α : Type u_1
β : Type ?u.419875
γ : Type ?u.419878
inst✝ : PseudoEMetricSpace α
f : α → ℝ≥0∞
C : ℝ≥0∞
hC : C ≠ ⊤
h : ∀ (x y : α), f x ≤ f y + C * edist x y
x : α
ε : ℝ≥0∞
ε0 : ε > 0
δ : ℝ≥0
δ0 : δ > 0
hδ : ↑δ * C < ε
⊢ ∀ᶠ (x_1 : α) in 𝓝 x, f x_1 ∈ Icc (f x - ε) (f x + ε)
α : Type u_1
β : Type ?u.419875
γ : Type ?u.419878
inst✝ : PseudoEMetricSpace α
f : α → ℝ≥0∞
C : ℝ≥0∞
hC : C ≠ ⊤
h : ∀ (x y : α), f x ≤ f y + C * edist x y
x : α
ε : ℝ≥0∞
ε0 : ε > 0
⊢ ∀ᶠ (x_1 : α) in 𝓝 x, f x_1 ∈ Icc (f x - ε) (f x + ε)
rcases ENNReal.exists_nnreal_pos_mul_lt hC ε0.ne' with ⟨δ, δ0, hδ⟩
case intro.intro
α : Type u_1
β : Type ?u.419875
γ : Type ?u.419878
inst✝ : PseudoEMetricSpace α
f : α → ℝ≥0∞
C : ℝ≥0∞
hC : C ≠ ⊤
h : ∀ (x y : α), f x ≤ f y + C * edist x y
x : α
ε : ℝ≥0∞
ε0 : ε > 0
δ : ℝ≥0
δ0 : δ > 0
hδ : C * ↑δ < ε
⊢ ∀ᶠ (x_1 : α) in 𝓝 x, f x_1 ∈ Icc (f x - ε) (f x + ε)
case intro.intro
α : Type u_1
β : Type ?u.419875
γ : Type ?u.419878
inst✝ : PseudoEMetricSpace α
f : α → ℝ≥0∞
C : ℝ≥0∞
hC : C ≠ ⊤
h : ∀ (x y : α), f x ≤ f y + C * edist x y
x : α
ε : ℝ≥0∞
ε0 : ε > 0
δ : ℝ≥0
δ0 : δ > 0
hδ : ↑δ * C < ε
⊢ ∀ᶠ (x_1 : α) in 𝓝 x, f x_1 ∈ Icc (f x - ε) (f x + ε)
rw [mul_comm] at hδ
case h
α : Type u_1
β : Type ?u.419875
γ : Type ?u.419878
inst✝ : PseudoEMetricSpace α
f : α → ℝ≥0∞
C : ℝ≥0∞
hC : C ≠ ⊤
h : ∀ (x y : α), f x ≤ f y + C * edist x y
x : α
ε : ℝ≥0∞
ε0 : ε > 0
δ : ℝ≥0
δ0 : δ > 0
hδ : C * ↑δ < ε
y : α
hy : y ∈ EMetric.closedBall x ↑δ
⊢ f y ∈ Icc (f x - ε) (f x + ε)
case intro.intro
α : Type u_1
β : Type ?u.419875
γ : Type ?u.419878
inst✝ : PseudoEMetricSpace α
f : α → ℝ≥0∞
C : ℝ≥0∞
hC : C ≠ ⊤
h : ∀ (x y : α), f x ≤ f y + C * edist x y
x : α
ε : ℝ≥0∞
ε0 : ε > 0
δ : ℝ≥0
δ0 : δ > 0
hδ : C * ↑δ < ε
⊢ ∀ᶠ (x_1 : α) in 𝓝 x, f x_1 ∈ Icc (f x - ε) (f x + ε)
filter_upwards [EMetric.closedBall_mem_nhds x (ENNReal.coe_pos.2 δ0)] with y hy
case h.refine_1
α : Type u_1
β : Type ?u.419875
γ : Type ?u.419878
inst✝ : PseudoEMetricSpace α
f : α → ℝ≥0∞
C : ℝ≥0∞
hC : C ≠ ⊤
h : ∀ (x y : α), f x ≤ f y + C * edist x y
x : α
ε : ℝ≥0∞
ε0 : ε > 0
δ : ℝ≥0
δ0 : δ > 0
hδ : C * ↑δ < ε
y : α
hy : y ∈ EMetric.closedBall x ↑δ
⊢ edist x y ≤ ↑δ

case h.refine_2
α : Type u_1
β : Type ?u.419875
γ : Type ?u.419878
inst✝ : PseudoEMetricSpace α
f : α → ℝ≥0∞
C : ℝ≥0∞
hC : C ≠ ⊤
h : ∀ (x y : α), f x ≤ f y + C * edist x y
x : α
ε : ℝ≥0∞
ε0 : ε > 0
δ : ℝ≥0
δ0 : δ > 0
hδ : C * ↑δ < ε
y : α
hy : y ∈ EMetric.closedBall x ↑δ
⊢ edist y x ≤ ↑δ
case h
α : Type u_1
β : Type ?u.419875
γ : Type ?u.419878
inst✝ : PseudoEMetricSpace α
f : α → ℝ≥0∞
C : ℝ≥0∞
hC : C ≠ ⊤
h : ∀ (x y : α), f x ≤ f y + C * edist x y
x : α
ε : ℝ≥0∞
ε0 : ε > 0
δ : ℝ≥0
δ0 : δ > 0
hδ : C * ↑δ < ε
y : α
hy : y ∈ EMetric.closedBall x ↑δ
⊢ f y ∈ Icc (f x - ε) (f x + ε)
refine ⟨tsub_le_iff_right.2 <| (h x y).trans ?_, (h y x).trans ?_⟩ <;>
  refine add_le_add_left (le_trans (mul_le_mul_left' ?_ _) hδ.le) _
no goals
case h.refine_1
α : Type u_1
β : Type ?u.419875
γ : Type ?u.419878
inst✝ : PseudoEMetricSpace α
f : α → ℝ≥0∞
C : ℝ≥0∞
hC : C ≠ ⊤
h : ∀ (x y : α), f x ≤ f y + C * edist x y
x : α
ε : ℝ≥0∞
ε0 : ε > 0
δ : ℝ≥0
δ0 : δ > 0
hδ : C * ↑δ < ε
y : α
hy : y ∈ EMetric.closedBall x ↑δ
⊢ edist x y ≤ ↑δ

case h.refine_2
α : Type u_1
β : Type ?u.419875
γ : Type ?u.419878
inst✝ : PseudoEMetricSpace α
f : α → ℝ≥0∞
C : ℝ≥0∞
hC : C ≠ ⊤
h : ∀ (x y : α), f x ≤ f y + C * edist x y
x : α
ε : ℝ≥0∞
ε0 : ε > 0
δ : ℝ≥0
δ0 : δ > 0
hδ : C * ↑δ < ε
y : α
hy : y ∈ EMetric.closedBall x ↑δ
⊢ edist y x ≤ ↑δ
exacts [EMetric.mem_closedBall'.1 hy, EMetric.mem_closedBall.1 hy]