ι : Sort ?u.11409
α : Type u
β : Type v
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
x y : α
s t : Set α
Φ : α → β
⊢ infEdist x s ≤ infEdist x (closure s)
ι : Sort ?u.11409
α : Type u
β : Type v
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
x y : α
s t : Set α
Φ : α → β
⊢ infEdist x (closure s) = infEdist x s
refine' le_antisymm (infEdist_anti subset_closure) _
ι : Sort ?u.11409
α : Type u
β : Type v
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
x y : α
s t : Set α
Φ : α → β
ε : ℝ≥0
εpos : 0 < ε
h : infEdist x (closure s) < ⊤
⊢ infEdist x s ≤ infEdist x (closure s) + ↑ε
ι : Sort ?u.11409
α : Type u
β : Type v
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
x y : α
s t : Set α
Φ : α → β
⊢ infEdist x s ≤ infEdist x (closure s)
refine' ENNReal.le_of_forall_pos_le_add fun ε εpos h => _
ι : Sort ?u.11409
α : Type u
β : Type v
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
x y : α
s t : Set α
Φ : α → β
ε : ℝ≥0
εpos : 0 < ε
h : infEdist x (closure s) < ⊤
ε0 : 0 < ↑ε / 2
⊢ infEdist x s ≤ infEdist x (closure s) + ↑ε
ι : Sort ?u.11409
α : Type u
β : Type v
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
x y : α
s t : Set α
Φ : α → β
ε : ℝ≥0
εpos : 0 < ε
h : infEdist x (closure s) < ⊤
⊢ infEdist x s ≤ infEdist x (closure s) + ↑ε
have ε0 : 0 < (ε / 2 : ℝ≥0∞) := by simpa [pos_iff_ne_zero] using εpos
ι : Sort ?u.11409
α : Type u
β : Type v
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
x y : α
s t : Set α
Φ : α → β
ε : ℝ≥0
εpos : 0 < ε
h : infEdist x (closure s) < ⊤
ε0 : 0 < ↑ε / 2
this : infEdist x (closure s) < infEdist x (closure s) + ↑ε / 2
⊢ infEdist x s ≤ infEdist x (closure s) + ↑ε
ι : Sort ?u.11409
α : Type u
β : Type v
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
x y : α
s t : Set α
Φ : α → β
ε : ℝ≥0
εpos : 0 < ε
h : infEdist x (closure s) < ⊤
ε0 : 0 < ↑ε / 2
⊢ infEdist x s ≤ infEdist x (closure s) + ↑ε
have : infEdist x (closure s) < infEdist x (closure s) + ε / 2 :=
  ENNReal.lt_add_right h.ne ε0.ne'
case intro.intro
ι : Sort ?u.11409
α : Type u
β : Type v
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
x y✝ : α
s t : Set α
Φ : α → β
ε : ℝ≥0
εpos : 0 < ε
h : infEdist x (closure s) < ⊤
ε0 : 0 < ↑ε / 2
this : infEdist x (closure s) < infEdist x (closure s) + ↑ε / 2
y : α
ycs : y ∈ closure s
hy : edist x y < infEdist x (closure s) + ↑ε / 2
⊢ infEdist x s ≤ infEdist x (closure s) + ↑ε
ι : Sort ?u.11409
α : Type u
β : Type v
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
x y : α
s t : Set α
Φ : α → β
ε : ℝ≥0
εpos : 0 < ε
h : infEdist x (closure s) < ⊤
ε0 : 0 < ↑ε / 2
this : infEdist x (closure s) < infEdist x (closure s) + ↑ε / 2
⊢ infEdist x s ≤ infEdist x (closure s) + ↑ε
rcases infEdist_lt_iff.mp this with ⟨y, ycs, hy⟩
case intro.intro.intro.intro
ι : Sort ?u.11409
α : Type u
β : Type v
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
x y✝ : α
s t : Set α
Φ : α → β
ε : ℝ≥0
εpos : 0 < ε
h : infEdist x (closure s) < ⊤
ε0 : 0 < ↑ε / 2
this : infEdist x (closure s) < infEdist x (closure s) + ↑ε / 2
y : α
ycs : y ∈ closure s
hy : edist x y < infEdist x (closure s) + ↑ε / 2
z : α
zs : z ∈ s
dyz : edist y z < ↑ε / 2
⊢ infEdist x s ≤ infEdist x (closure s) + ↑ε
case intro.intro
ι : Sort ?u.11409
α : Type u
β : Type v
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
x y✝ : α
s t : Set α
Φ : α → β
ε : ℝ≥0
εpos : 0 < ε
h : infEdist x (closure s) < ⊤
ε0 : 0 < ↑ε / 2
this : infEdist x (closure s) < infEdist x (closure s) + ↑ε / 2
y : α
ycs : y ∈ closure s
hy : edist x y < infEdist x (closure s) + ↑ε / 2
⊢ infEdist x s ≤ infEdist x (closure s) + ↑ε
rcases EMetric.mem_closure_iff.1 ycs (ε / 2) ε0 with ⟨z, zs, dyz⟩
no goals
case intro.intro.intro.intro
ι : Sort ?u.11409
α : Type u
β : Type v
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
x y✝ : α
s t : Set α
Φ : α → β
ε : ℝ≥0
εpos : 0 < ε
h : infEdist x (closure s) < ⊤
ε0 : 0 < ↑ε / 2
this : infEdist x (closure s) < infEdist x (closure s) + ↑ε / 2
y : α
ycs : y ∈ closure s
hy : edist x y < infEdist x (closure s) + ↑ε / 2
z : α
zs : z ∈ s
dyz : edist y z < ↑ε / 2
⊢ infEdist x s ≤ infEdist x (closure s) + ↑ε
calc
  infEdist x s ≤ edist x z := infEdist_le_edist_of_mem zs
  _ ≤ edist x y + edist y z := (edist_triangle _ _ _)
  _ ≤ infEdist x (closure s) + ε / 2 + ε / 2 := (add_le_add (le_of_lt hy) (le_of_lt dyz))
  _ = infEdist x (closure s) + ↑ε := by rw [add_assoc, ENNReal.add_halves]
no goals
ι : Sort ?u.11409
α : Type u
β : Type v
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
x y : α
s t : Set α
Φ : α → β
ε : ℝ≥0
εpos : 0 < ε
h : infEdist x (closure s) < ⊤
⊢ 0 < ↑ε / 2
simpa [pos_iff_ne_zero] using εpos
no goals
ι : Sort ?u.11409
α : Type u
β : Type v
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
x y✝ : α
s t : Set α
Φ : α → β
ε : ℝ≥0
εpos : 0 < ε
h : infEdist x (closure s) < ⊤
ε0 : 0 < ↑ε / 2
this : infEdist x (closure s) < infEdist x (closure s) + ↑ε / 2
y : α
ycs : y ∈ closure s
hy : edist x y < infEdist x (closure s) + ↑ε / 2
z : α
zs : z ∈ s
dyz : edist y z < ↑ε / 2
⊢ infEdist x (closure s) + ↑ε / 2 + ↑ε / 2 = infEdist x (closure s) + ↑ε
rw [add_assoc, ENNReal.add_halves]