[GOAL]
ι : Sort u_1
α : Type u
β : Type v
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
x y : α
s t : Set α
Φ : α → β
d : ℝ≥0∞
⊢ d ≤ infEdist x s ↔ ∀ (y : α), y ∈ s → d ≤ edist x y
[PROOFSTEP]
simp only [infEdist, le_iInf_iff]
[GOAL]
ι : Sort u_1
α : Type u
β : Type v
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
x y : α
s t : Set α
Φ : α → β
r : ℝ≥0∞
⊢ infEdist x s < r ↔ ∃ y, y ∈ s ∧ edist x y < r
[PROOFSTEP]
simp_rw [infEdist, iInf_lt_iff, exists_prop]
[GOAL]
ι : Sort u_1
α : Type u
β : Type v
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
x y : α
s t : Set α
Φ : α → β
⊢ ⨅ (z : α) (_ : z ∈ s), edist y z + edist x y = (⨅ (z : α) (_ : z ∈ s), edist y z) + edist x y
[PROOFSTEP]
simp only [ENNReal.iInf_add]
[GOAL]
ι : Sort u_1
α : Type u
β : Type v
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
x y : α
s t : Set α
Φ : α → β
⊢ infEdist x s ≤ edist x y + infEdist y s
[PROOFSTEP]
rw [add_comm]
[GOAL]
ι : Sort u_1
α : Type u
β : Type v
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
x y : α
s t : Set α
Φ : α → β
⊢ infEdist x s ≤ infEdist y s + edist x y
[PROOFSTEP]
exact infEdist_le_infEdist_add_edist
[GOAL]
ι : Sort u_1
α : Type u
β : Type v
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
x y : α
s t : Set α
Φ : α → β
hy : y ∈ s
⊢ edist x y ≤ infEdist x s + diam s
[PROOFSTEP]
simp_rw [infEdist, ENNReal.iInf_add]
[GOAL]
ι : Sort u_1
α : Type u
β : Type v
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
x y : α
s t : Set α
Φ : α → β
hy : y ∈ s
⊢ edist x y ≤ ⨅ (i : α) (_ : i ∈ s), edist x i + diam s
[PROOFSTEP]
refine le_iInf₂ fun i hi => ?_
[GOAL]
ι : Sort u_1
α : Type u
β : Type v
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
x y : α
s t : Set α
Φ : α → β
hy : y ∈ s
i : α
hi : i ∈ s
⊢ edist x y ≤ edist x i + diam s
[PROOFSTEP]
calc
  edist x y ≤ edist x i + edist i y := edist_triangle _ _ _
  _ ≤ edist x i + diam s := add_le_add le_rfl (edist_le_diam_of_mem hi hy)
[GOAL]
ι : Sort u_1
α : Type u
β : Type v
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
x y : α
s t : Set α
Φ : α → β
⊢ 1 ≠ ⊤
[PROOFSTEP]
simp
[GOAL]
ι : Sort u_1
α : Type u
β : Type v
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
x y : α
s t : Set α
Φ : α → β
⊢ ∀ (x y : α), infEdist x s ≤ infEdist y s + 1 * edist x y
[PROOFSTEP]
simp only [one_mul, infEdist_le_infEdist_add_edist, forall₂_true_iff]
[GOAL]
ι : Sort u_1
α : Type u
β : Type v
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
x y : α
s t : Set α
Φ : α → β
⊢ infEdist x (closure s) = infEdist x s
[PROOFSTEP]
refine' le_antisymm (infEdist_anti subset_closure) _
[GOAL]
ι : Sort u_1
α : Type u
β : Type v
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
x y : α
s t : Set α
Φ : α → β
⊢ infEdist x s ≤ infEdist x (closure s)
[PROOFSTEP]
refine' ENNReal.le_of_forall_pos_le_add fun ε εpos h => _
[GOAL]
ι : Sort u_1
α : 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) + ↑ε
[PROOFSTEP]
have ε0 : 0 < (ε / 2 : ℝ≥0∞) := by simpa [pos_iff_ne_zero] using εpos
[GOAL]
ι : Sort u_1
α : Type u
β : Type v
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
x y : α
s t : Set α
Φ : α → β
ε : ℝ≥0
εpos : 0 < ε
h : infEdist x (closure s) < ⊤
⊢ 0 < ↑ε / 2
[PROOFSTEP]
simpa [pos_iff_ne_zero] using εpos
[GOAL]
ι : Sort u_1
α : 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) + ↑ε
[PROOFSTEP]
have : infEdist x (closure s) < infEdist x (closure s) + ε / 2 := ENNReal.lt_add_right h.ne ε0.ne'
[GOAL]
ι : Sort u_1
α : 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) + ↑ε
[PROOFSTEP]
rcases infEdist_lt_iff.mp this with
  ⟨y, ycs, hy⟩
    -- y : α, ycs : y ∈ closure s, hy : edist x y < infEdist x (closure s) + ↑ε / 2
[GOAL]
case intro.intro
ι : Sort u_1
α : 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) + ↑ε
[PROOFSTEP]
rcases EMetric.mem_closure_iff.1 ycs (ε / 2) ε0 with
  ⟨z, zs, dyz⟩
    -- z : α, zs : z ∈ s, dyz : edist y z < ↑ε / 2
[GOAL]
case intro.intro.intro.intro
ι : Sort u_1
α : 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) + ↑ε
[PROOFSTEP]
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]
[GOAL]
ι : Sort u_1
α : 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) + ↑ε
[PROOFSTEP]
rw [add_assoc, ENNReal.add_halves]
[GOAL]
ι : Sort u_1
α : Type u
β : Type v
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
x y : α
s t : Set α
Φ : α → β
h : x ∈ closure s
⊢ infEdist x s = 0
[PROOFSTEP]
rw [← infEdist_closure]
[GOAL]
ι : Sort u_1
α : Type u
β : Type v
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
x y : α
s t : Set α
Φ : α → β
h : x ∈ closure s
⊢ infEdist x (closure s) = 0
[PROOFSTEP]
exact infEdist_zero_of_mem h
[GOAL]
ι : Sort u_1
α : Type u
β : Type v
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
x y : α
s t : Set α
Φ : α → β
h : infEdist x s = 0
ε : ℝ≥0∞
εpos : ε > 0
⊢ infEdist x s < ε
[PROOFSTEP]
rwa [h]
[GOAL]
ι : Sort u_1
α : Type u
β : Type v
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
x y : α
s t : Set α
Φ : α → β
h : IsClosed s
⊢ x ∈ s ↔ infEdist x s = 0
[PROOFSTEP]
rw [← mem_closure_iff_infEdist_zero, h.closure_eq]
[GOAL]
ι : Sort u_1
α : Type u
β : Type v
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
x✝ y : α
s t : Set α
Φ : α → β
x : α
E : Set α
⊢ 0 < infEdist x E ↔ ¬x ∈ closure E
[PROOFSTEP]
rw [mem_closure_iff_infEdist_zero, pos_iff_ne_zero]
[GOAL]
ι : Sort u_1
α : Type u
β : Type v
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
x✝ y : α
s t : Set α
Φ : α → β
x : α
E : Set α
⊢ 0 < infEdist x (closure E) ↔ ¬x ∈ closure E
[PROOFSTEP]
rw [infEdist_closure, infEdist_pos_iff_not_mem_closure]
[GOAL]
ι : Sort u_1
α : Type u
β : Type v
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
x✝ y : α
s t : Set α
Φ : α → β
x : α
E : Set α
h : ¬x ∈ closure E
⊢ ∃ ε, 0 < ε ∧ ENNReal.ofReal ε < infEdist x E
[PROOFSTEP]
rw [← infEdist_pos_iff_not_mem_closure, ENNReal.lt_iff_exists_real_btwn] at h 
[GOAL]
ι : Sort u_1
α : Type u
β : Type v
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
x✝ y : α
s t : Set α
Φ : α → β
x : α
E : Set α
h : ∃ r, 0 ≤ r ∧ 0 < ENNReal.ofReal r ∧ ENNReal.ofReal r < infEdist x E
⊢ ∃ ε, 0 < ε ∧ ENNReal.ofReal ε < infEdist x E
[PROOFSTEP]
rcases h with ⟨ε, ⟨_, ⟨ε_pos, ε_lt⟩⟩⟩
[GOAL]
case intro.intro.intro
ι : Sort u_1
α : Type u
β : Type v
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
x✝ y : α
s t : Set α
Φ : α → β
x : α
E : Set α
ε : ℝ
left✝ : 0 ≤ ε
ε_pos : 0 < ENNReal.ofReal ε
ε_lt : ENNReal.ofReal ε < infEdist x E
⊢ ∃ ε, 0 < ε ∧ ENNReal.ofReal ε < infEdist x E
[PROOFSTEP]
exact ⟨ε, ⟨ENNReal.ofReal_pos.mp ε_pos, ε_lt⟩⟩
[GOAL]
ι : Sort u_1
α : Type u
β : Type v
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
x y : α
s t : Set α
Φ : α → β
r : ℝ≥0∞
h : r < infEdist x s
⊢ Disjoint (closedBall x r) s
[PROOFSTEP]
rw [disjoint_left]
[GOAL]
ι : Sort u_1
α : Type u
β : Type v
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
x y : α
s t : Set α
Φ : α → β
r : ℝ≥0∞
h : r < infEdist x s
⊢ ∀ ⦃a : α⦄, a ∈ closedBall x r → ¬a ∈ s
[PROOFSTEP]
intro y hy h'y
[GOAL]
ι : Sort u_1
α : Type u
β : Type v
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
x y✝ : α
s t : Set α
Φ : α → β
r : ℝ≥0∞
h : r < infEdist x s
y : α
hy : y ∈ closedBall x r
h'y : y ∈ s
⊢ False
[PROOFSTEP]
apply lt_irrefl (infEdist x s)
[GOAL]
ι : Sort u_1
α : Type u
β : Type v
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
x y✝ : α
s t : Set α
Φ : α → β
r : ℝ≥0∞
h : r < infEdist x s
y : α
hy : y ∈ closedBall x r
h'y : y ∈ s
⊢ infEdist x s < infEdist x s
[PROOFSTEP]
calc
  infEdist x s ≤ edist x y := infEdist_le_edist_of_mem h'y
  _ ≤ r := by rwa [mem_closedBall, edist_comm] at hy 
  _ < infEdist x s := h
[GOAL]
ι : Sort u_1
α : Type u
β : Type v
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
x y✝ : α
s t : Set α
Φ : α → β
r : ℝ≥0∞
h : r < infEdist x s
y : α
hy : y ∈ closedBall x r
h'y : y ∈ s
⊢ edist x y ≤ r
[PROOFSTEP]
rwa [mem_closedBall, edist_comm] at hy 
[GOAL]
ι : Sort u_1
α : Type u
β : Type v
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
x y : α
s t : Set α
Φ : α → β
hΦ : Isometry Φ
⊢ infEdist (Φ x) (Φ '' t) = infEdist x t
[PROOFSTEP]
simp only [infEdist, iInf_image, hΦ.edist_eq]
[GOAL]
ι : Sort u_1
α : Type u
β : Type v
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
x y : α
s t : Set α
Φ : α → β
U : Set α
hU : IsOpen U
⊢ ∃ F, (∀ (n : ℕ), IsClosed (F n)) ∧ (∀ (n : ℕ), F n ⊆ U) ∧ ⋃ (n : ℕ), F n = U ∧ Monotone F
[PROOFSTEP]
obtain ⟨a, a_pos, a_lt_one⟩ : ∃ a : ℝ≥0∞, 0 < a ∧ a < 1 := exists_between zero_lt_one
[GOAL]
case intro.intro
ι : Sort u_1
α : Type u
β : Type v
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
x y : α
s t : Set α
Φ : α → β
U : Set α
hU : IsOpen U
a : ℝ≥0∞
a_pos : 0 < a
a_lt_one : a < 1
⊢ ∃ F, (∀ (n : ℕ), IsClosed (F n)) ∧ (∀ (n : ℕ), F n ⊆ U) ∧ ⋃ (n : ℕ), F n = U ∧ Monotone F
[PROOFSTEP]
let F := fun n : ℕ => (fun x => infEdist x Uᶜ) ⁻¹' Ici (a ^ n)
[GOAL]
case intro.intro
ι : Sort u_1
α : Type u
β : Type v
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
x y : α
s t : Set α
Φ : α → β
U : Set α
hU : IsOpen U
a : ℝ≥0∞
a_pos : 0 < a
a_lt_one : a < 1
F : ℕ → Set α := fun n => (fun x => infEdist x Uᶜ) ⁻¹' Ici (a ^ n)
⊢ ∃ F, (∀ (n : ℕ), IsClosed (F n)) ∧ (∀ (n : ℕ), F n ⊆ U) ∧ ⋃ (n : ℕ), F n = U ∧ Monotone F
[PROOFSTEP]
have F_subset : ∀ n, F n ⊆ U := fun n x hx ↦ by
  by_contra h
  have : infEdist x Uᶜ ≠ 0 := ((ENNReal.pow_pos a_pos _).trans_le hx).ne'
  exact this (infEdist_zero_of_mem h)
[GOAL]
ι : Sort u_1
α : Type u
β : Type v
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
x✝ y : α
s t : Set α
Φ : α → β
U : Set α
hU : IsOpen U
a : ℝ≥0∞
a_pos : 0 < a
a_lt_one : a < 1
F : ℕ → Set α := fun n => (fun x => infEdist x Uᶜ) ⁻¹' Ici (a ^ n)
n : ℕ
x : α
hx : x ∈ F n
⊢ x ∈ U
[PROOFSTEP]
by_contra h
[GOAL]
ι : Sort u_1
α : Type u
β : Type v
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
x✝ y : α
s t : Set α
Φ : α → β
U : Set α
hU : IsOpen U
a : ℝ≥0∞
a_pos : 0 < a
a_lt_one : a < 1
F : ℕ → Set α := fun n => (fun x => infEdist x Uᶜ) ⁻¹' Ici (a ^ n)
n : ℕ
x : α
hx : x ∈ F n
h : ¬x ∈ U
⊢ False
[PROOFSTEP]
have : infEdist x Uᶜ ≠ 0 := ((ENNReal.pow_pos a_pos _).trans_le hx).ne'
[GOAL]
ι : Sort u_1
α : Type u
β : Type v
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
x✝ y : α
s t : Set α
Φ : α → β
U : Set α
hU : IsOpen U
a : ℝ≥0∞
a_pos : 0 < a
a_lt_one : a < 1
F : ℕ → Set α := fun n => (fun x => infEdist x Uᶜ) ⁻¹' Ici (a ^ n)
n : ℕ
x : α
hx : x ∈ F n
h : ¬x ∈ U
this : infEdist x Uᶜ ≠ 0
⊢ False
[PROOFSTEP]
exact this (infEdist_zero_of_mem h)
[GOAL]
case intro.intro
ι : Sort u_1
α : Type u
β : Type v
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
x y : α
s t : Set α
Φ : α → β
U : Set α
hU : IsOpen U
a : ℝ≥0∞
a_pos : 0 < a
a_lt_one : a < 1
F : ℕ → Set α := fun n => (fun x => infEdist x Uᶜ) ⁻¹' Ici (a ^ n)
F_subset : ∀ (n : ℕ), F n ⊆ U
⊢ ∃ F, (∀ (n : ℕ), IsClosed (F n)) ∧ (∀ (n : ℕ), F n ⊆ U) ∧ ⋃ (n : ℕ), F n = U ∧ Monotone F
[PROOFSTEP]
refine ⟨F, fun n => IsClosed.preimage continuous_infEdist isClosed_Ici, F_subset, ?_, ?_⟩
[GOAL]
case intro.intro.refine_1
ι : Sort u_1
α : Type u
β : Type v
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
x y : α
s t : Set α
Φ : α → β
U : Set α
hU : IsOpen U
a : ℝ≥0∞
a_pos : 0 < a
a_lt_one : a < 1
F : ℕ → Set α := fun n => (fun x => infEdist x Uᶜ) ⁻¹' Ici (a ^ n)
F_subset : ∀ (n : ℕ), F n ⊆ U
⊢ ⋃ (n : ℕ), F n = U
case intro.intro.refine_2
ι : Sort u_1
α : Type u
β : Type v
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
x y : α
s t : Set α
Φ : α → β
U : Set α
hU : IsOpen U
a : ℝ≥0∞
a_pos : 0 < a
a_lt_one : a < 1
F : ℕ → Set α := fun n => (fun x => infEdist x Uᶜ) ⁻¹' Ici (a ^ n)
F_subset : ∀ (n : ℕ), F n ⊆ U
⊢ Monotone F
[PROOFSTEP]
show ⋃ n, F n = U
[GOAL]
case intro.intro.refine_1
ι : Sort u_1
α : Type u
β : Type v
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
x y : α
s t : Set α
Φ : α → β
U : Set α
hU : IsOpen U
a : ℝ≥0∞
a_pos : 0 < a
a_lt_one : a < 1
F : ℕ → Set α := fun n => (fun x => infEdist x Uᶜ) ⁻¹' Ici (a ^ n)
F_subset : ∀ (n : ℕ), F n ⊆ U
⊢ ⋃ (n : ℕ), F n = U
[PROOFSTEP]
refine' Subset.antisymm (by simp only [iUnion_subset_iff, F_subset, forall_const]) fun x hx => _
[GOAL]
ι : Sort u_1
α : Type u
β : Type v
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
x y : α
s t : Set α
Φ : α → β
U : Set α
hU : IsOpen U
a : ℝ≥0∞
a_pos : 0 < a
a_lt_one : a < 1
F : ℕ → Set α := fun n => (fun x => infEdist x Uᶜ) ⁻¹' Ici (a ^ n)
F_subset : ∀ (n : ℕ), F n ⊆ U
⊢ ⋃ (n : ℕ), F n ⊆ U
[PROOFSTEP]
simp only [iUnion_subset_iff, F_subset, forall_const]
[GOAL]
case intro.intro.refine_1
ι : Sort u_1
α : Type u
β : Type v
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
x✝ y : α
s t : Set α
Φ : α → β
U : Set α
hU : IsOpen U
a : ℝ≥0∞
a_pos : 0 < a
a_lt_one : a < 1
F : ℕ → Set α := fun n => (fun x => infEdist x Uᶜ) ⁻¹' Ici (a ^ n)
F_subset : ∀ (n : ℕ), F n ⊆ U
x : α
hx : x ∈ U
⊢ x ∈ ⋃ (n : ℕ), F n
[PROOFSTEP]
have : ¬x ∈ Uᶜ := by simpa using hx
[GOAL]
ι : Sort u_1
α : Type u
β : Type v
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
x✝ y : α
s t : Set α
Φ : α → β
U : Set α
hU : IsOpen U
a : ℝ≥0∞
a_pos : 0 < a
a_lt_one : a < 1
F : ℕ → Set α := fun n => (fun x => infEdist x Uᶜ) ⁻¹' Ici (a ^ n)
F_subset : ∀ (n : ℕ), F n ⊆ U
x : α
hx : x ∈ U
⊢ ¬x ∈ Uᶜ
[PROOFSTEP]
simpa using hx
[GOAL]
case intro.intro.refine_1
ι : Sort u_1
α : Type u
β : Type v
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
x✝ y : α
s t : Set α
Φ : α → β
U : Set α
hU : IsOpen U
a : ℝ≥0∞
a_pos : 0 < a
a_lt_one : a < 1
F : ℕ → Set α := fun n => (fun x => infEdist x Uᶜ) ⁻¹' Ici (a ^ n)
F_subset : ∀ (n : ℕ), F n ⊆ U
x : α
hx : x ∈ U
this : ¬x ∈ Uᶜ
⊢ x ∈ ⋃ (n : ℕ), F n
[PROOFSTEP]
rw [mem_iff_infEdist_zero_of_closed hU.isClosed_compl] at this 
[GOAL]
case intro.intro.refine_1
ι : Sort u_1
α : Type u
β : Type v
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
x✝ y : α
s t : Set α
Φ : α → β
U : Set α
hU : IsOpen U
a : ℝ≥0∞
a_pos : 0 < a
a_lt_one : a < 1
F : ℕ → Set α := fun n => (fun x => infEdist x Uᶜ) ⁻¹' Ici (a ^ n)
F_subset : ∀ (n : ℕ), F n ⊆ U
x : α
hx : x ∈ U
this : ¬infEdist x Uᶜ = 0
⊢ x ∈ ⋃ (n : ℕ), F n
[PROOFSTEP]
have B : 0 < infEdist x Uᶜ := by simpa [pos_iff_ne_zero] using this
[GOAL]
ι : Sort u_1
α : Type u
β : Type v
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
x✝ y : α
s t : Set α
Φ : α → β
U : Set α
hU : IsOpen U
a : ℝ≥0∞
a_pos : 0 < a
a_lt_one : a < 1
F : ℕ → Set α := fun n => (fun x => infEdist x Uᶜ) ⁻¹' Ici (a ^ n)
F_subset : ∀ (n : ℕ), F n ⊆ U
x : α
hx : x ∈ U
this : ¬infEdist x Uᶜ = 0
⊢ 0 < infEdist x Uᶜ
[PROOFSTEP]
simpa [pos_iff_ne_zero] using this
[GOAL]
case intro.intro.refine_1
ι : Sort u_1
α : Type u
β : Type v
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
x✝ y : α
s t : Set α
Φ : α → β
U : Set α
hU : IsOpen U
a : ℝ≥0∞
a_pos : 0 < a
a_lt_one : a < 1
F : ℕ → Set α := fun n => (fun x => infEdist x Uᶜ) ⁻¹' Ici (a ^ n)
F_subset : ∀ (n : ℕ), F n ⊆ U
x : α
hx : x ∈ U
this : ¬infEdist x Uᶜ = 0
B : 0 < infEdist x Uᶜ
⊢ x ∈ ⋃ (n : ℕ), F n
[PROOFSTEP]
have : Filter.Tendsto (fun n => a ^ n) atTop (𝓝 0) := ENNReal.tendsto_pow_atTop_nhds_0_of_lt_1 a_lt_one
[GOAL]
case intro.intro.refine_1
ι : Sort u_1
α : Type u
β : Type v
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
x✝ y : α
s t : Set α
Φ : α → β
U : Set α
hU : IsOpen U
a : ℝ≥0∞
a_pos : 0 < a
a_lt_one : a < 1
F : ℕ → Set α := fun n => (fun x => infEdist x Uᶜ) ⁻¹' Ici (a ^ n)
F_subset : ∀ (n : ℕ), F n ⊆ U
x : α
hx : x ∈ U
this✝ : ¬infEdist x Uᶜ = 0
B : 0 < infEdist x Uᶜ
this : Tendsto (fun n => a ^ n) atTop (𝓝 0)
⊢ x ∈ ⋃ (n : ℕ), F n
[PROOFSTEP]
rcases((tendsto_order.1 this).2 _ B).exists with ⟨n, hn⟩
[GOAL]
case intro.intro.refine_1.intro
ι : Sort u_1
α : Type u
β : Type v
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
x✝ y : α
s t : Set α
Φ : α → β
U : Set α
hU : IsOpen U
a : ℝ≥0∞
a_pos : 0 < a
a_lt_one : a < 1
F : ℕ → Set α := fun n => (fun x => infEdist x Uᶜ) ⁻¹' Ici (a ^ n)
F_subset : ∀ (n : ℕ), F n ⊆ U
x : α
hx : x ∈ U
this✝ : ¬infEdist x Uᶜ = 0
B : 0 < infEdist x Uᶜ
this : Tendsto (fun n => a ^ n) atTop (𝓝 0)
n : ℕ
hn : a ^ n < infEdist x Uᶜ
⊢ x ∈ ⋃ (n : ℕ), F n
[PROOFSTEP]
simp only [mem_iUnion, mem_Ici, mem_preimage]
[GOAL]
case intro.intro.refine_1.intro
ι : Sort u_1
α : Type u
β : Type v
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
x✝ y : α
s t : Set α
Φ : α → β
U : Set α
hU : IsOpen U
a : ℝ≥0∞
a_pos : 0 < a
a_lt_one : a < 1
F : ℕ → Set α := fun n => (fun x => infEdist x Uᶜ) ⁻¹' Ici (a ^ n)
F_subset : ∀ (n : ℕ), F n ⊆ U
x : α
hx : x ∈ U
this✝ : ¬infEdist x Uᶜ = 0
B : 0 < infEdist x Uᶜ
this : Tendsto (fun n => a ^ n) atTop (𝓝 0)
n : ℕ
hn : a ^ n < infEdist x Uᶜ
⊢ ∃ i, a ^ i ≤ infEdist x Uᶜ
[PROOFSTEP]
exact ⟨n, hn.le⟩
[GOAL]
case intro.intro.refine_2
ι : Sort u_1
α : Type u
β : Type v
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
x y : α
s t : Set α
Φ : α → β
U : Set α
hU : IsOpen U
a : ℝ≥0∞
a_pos : 0 < a
a_lt_one : a < 1
F : ℕ → Set α := fun n => (fun x => infEdist x Uᶜ) ⁻¹' Ici (a ^ n)
F_subset : ∀ (n : ℕ), F n ⊆ U
⊢ Monotone F
[PROOFSTEP]
show Monotone F
[GOAL]
case intro.intro.refine_2
ι : Sort u_1
α : Type u
β : Type v
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
x y : α
s t : Set α
Φ : α → β
U : Set α
hU : IsOpen U
a : ℝ≥0∞
a_pos : 0 < a
a_lt_one : a < 1
F : ℕ → Set α := fun n => (fun x => infEdist x Uᶜ) ⁻¹' Ici (a ^ n)
F_subset : ∀ (n : ℕ), F n ⊆ U
⊢ Monotone F
[PROOFSTEP]
intro m n hmn x hx
[GOAL]
case intro.intro.refine_2
ι : Sort u_1
α : Type u
β : Type v
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
x✝ y : α
s t : Set α
Φ : α → β
U : Set α
hU : IsOpen U
a : ℝ≥0∞
a_pos : 0 < a
a_lt_one : a < 1
F : ℕ → Set α := fun n => (fun x => infEdist x Uᶜ) ⁻¹' Ici (a ^ n)
F_subset : ∀ (n : ℕ), F n ⊆ U
m n : ℕ
hmn : m ≤ n
x : α
hx : x ∈ F m
⊢ x ∈ F n
[PROOFSTEP]
simp only [mem_Ici, mem_preimage] at hx ⊢
[GOAL]
case intro.intro.refine_2
ι : Sort u_1
α : Type u
β : Type v
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
x✝ y : α
s t : Set α
Φ : α → β
U : Set α
hU : IsOpen U
a : ℝ≥0∞
a_pos : 0 < a
a_lt_one : a < 1
F : ℕ → Set α := fun n => (fun x => infEdist x Uᶜ) ⁻¹' Ici (a ^ n)
F_subset : ∀ (n : ℕ), F n ⊆ U
m n : ℕ
hmn : m ≤ n
x : α
hx : a ^ m ≤ infEdist x Uᶜ
⊢ a ^ n ≤ infEdist x Uᶜ
[PROOFSTEP]
apply le_trans (pow_le_pow_of_le_one' a_lt_one.le hmn) hx
[GOAL]
ι : Sort u_1
α : Type u
β : Type v
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
x✝ y : α
s t : Set α
Φ : α → β
hs : IsCompact s
hne : Set.Nonempty s
x : α
⊢ ∃ y, y ∈ s ∧ infEdist x s = edist x y
[PROOFSTEP]
have A : Continuous fun y => edist x y := continuous_const.edist continuous_id
[GOAL]
ι : Sort u_1
α : Type u
β : Type v
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
x✝ y : α
s t : Set α
Φ : α → β
hs : IsCompact s
hne : Set.Nonempty s
x : α
A : Continuous fun y => edist x y
⊢ ∃ y, y ∈ s ∧ infEdist x s = edist x y
[PROOFSTEP]
obtain ⟨y, ys, hy⟩ : ∃ y ∈ s, ∀ z, z ∈ s → edist x y ≤ edist x z := hs.exists_forall_le hne A.continuousOn
[GOAL]
case intro.intro
ι : Sort u_1
α : Type u
β : Type v
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
x✝ y✝ : α
s t : Set α
Φ : α → β
hs : IsCompact s
hne : Set.Nonempty s
x : α
A : Continuous fun y => edist x y
y : α
ys : y ∈ s
hy : ∀ (z : α), z ∈ s → edist x y ≤ edist x z
⊢ ∃ y, y ∈ s ∧ infEdist x s = edist x y
[PROOFSTEP]
exact ⟨y, ys, le_antisymm (infEdist_le_edist_of_mem ys) (by rwa [le_infEdist])⟩
[GOAL]
ι : Sort u_1
α : Type u
β : Type v
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
x✝ y✝ : α
s t : Set α
Φ : α → β
hs : IsCompact s
hne : Set.Nonempty s
x : α
A : Continuous fun y => edist x y
y : α
ys : y ∈ s
hy : ∀ (z : α), z ∈ s → edist x y ≤ edist x z
⊢ edist x y ≤ infEdist x s
[PROOFSTEP]
rwa [le_infEdist]
[GOAL]
ι : Sort u_1
α : Type u
β : Type v
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
x y : α
s t : Set α
Φ : α → β
hs : IsCompact s
ht : IsClosed t
hst : Disjoint s t
⊢ ∃ r, 0 < r ∧ ∀ (x : α), x ∈ s → ∀ (y : α), y ∈ t → ↑r < edist x y
[PROOFSTEP]
rcases s.eq_empty_or_nonempty with (rfl | hne)
[GOAL]
case inl
ι : Sort u_1
α : Type u
β : Type v
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
x y : α
t : Set α
Φ : α → β
ht : IsClosed t
hs : IsCompact ∅
hst : Disjoint ∅ t
⊢ ∃ r, 0 < r ∧ ∀ (x : α), x ∈ ∅ → ∀ (y : α), y ∈ t → ↑r < edist x y
[PROOFSTEP]
use 1
[GOAL]
case h
ι : Sort u_1
α : Type u
β : Type v
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
x y : α
t : Set α
Φ : α → β
ht : IsClosed t
hs : IsCompact ∅
hst : Disjoint ∅ t
⊢ 0 < 1 ∧ ∀ (x : α), x ∈ ∅ → ∀ (y : α), y ∈ t → ↑1 < edist x y
[PROOFSTEP]
simp
[GOAL]
case inr
ι : Sort u_1
α : Type u
β : Type v
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
x y : α
s t : Set α
Φ : α → β
hs : IsCompact s
ht : IsClosed t
hst : Disjoint s t
hne : Set.Nonempty s
⊢ ∃ r, 0 < r ∧ ∀ (x : α), x ∈ s → ∀ (y : α), y ∈ t → ↑r < edist x y
[PROOFSTEP]
obtain ⟨x, hx, h⟩ : ∃ x ∈ s, ∀ y ∈ s, infEdist x t ≤ infEdist y t :=
  hs.exists_forall_le hne continuous_infEdist.continuousOn
[GOAL]
case inr.intro.intro
ι : Sort u_1
α : Type u
β : Type v
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
x✝ y : α
s t : Set α
Φ : α → β
hs : IsCompact s
ht : IsClosed t
hst : Disjoint s t
hne : Set.Nonempty s
x : α
hx : x ∈ s
h : ∀ (y : α), y ∈ s → infEdist x t ≤ infEdist y t
⊢ ∃ r, 0 < r ∧ ∀ (x : α), x ∈ s → ∀ (y : α), y ∈ t → ↑r < edist x y
[PROOFSTEP]
have : 0 < infEdist x t := pos_iff_ne_zero.2 fun H => hst.le_bot ⟨hx, (mem_iff_infEdist_zero_of_closed ht).mpr H⟩
[GOAL]
case inr.intro.intro
ι : Sort u_1
α : Type u
β : Type v
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
x✝ y : α
s t : Set α
Φ : α → β
hs : IsCompact s
ht : IsClosed t
hst : Disjoint s t
hne : Set.Nonempty s
x : α
hx : x ∈ s
h : ∀ (y : α), y ∈ s → infEdist x t ≤ infEdist y t
this : 0 < infEdist x t
⊢ ∃ r, 0 < r ∧ ∀ (x : α), x ∈ s → ∀ (y : α), y ∈ t → ↑r < edist x y
[PROOFSTEP]
rcases ENNReal.lt_iff_exists_nnreal_btwn.1 this with ⟨r, h₀, hr⟩
[GOAL]
case inr.intro.intro.intro.intro
ι : Sort u_1
α : Type u
β : Type v
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
x✝ y : α
s t : Set α
Φ : α → β
hs : IsCompact s
ht : IsClosed t
hst : Disjoint s t
hne : Set.Nonempty s
x : α
hx : x ∈ s
h : ∀ (y : α), y ∈ s → infEdist x t ≤ infEdist y t
this : 0 < infEdist x t
r : ℝ≥0
h₀ : 0 < ↑r
hr : ↑r < infEdist x t
⊢ ∃ r, 0 < r ∧ ∀ (x : α), x ∈ s → ∀ (y : α), y ∈ t → ↑r < edist x y
[PROOFSTEP]
exact ⟨r, ENNReal.coe_pos.mp h₀, fun y hy z hz => hr.trans_le <| le_infEdist.1 (h y hy) z hz⟩
[GOAL]
ι : Sort u_1
α : Type u
β : Type v
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
x y : α
s t u : Set α
Φ : α → β
⊢ hausdorffEdist s s = 0
[PROOFSTEP]
simp only [hausdorffEdist_def, sup_idem, ENNReal.iSup_eq_zero]
[GOAL]
ι : Sort u_1
α : Type u
β : Type v
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
x y : α
s t u : Set α
Φ : α → β
⊢ ∀ (i : α), i ∈ s → infEdist i s = 0
[PROOFSTEP]
exact fun x hx => infEdist_zero_of_mem hx
[GOAL]
ι : Sort u_1
α : Type u
β : Type v
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
x y : α
s t u : Set α
Φ : α → β
⊢ hausdorffEdist s t = hausdorffEdist t s
[PROOFSTEP]
simp only [hausdorffEdist_def]
[GOAL]
ι : Sort u_1
α : Type u
β : Type v
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
x y : α
s t u : Set α
Φ : α → β
⊢ (⨆ (x : α) (_ : x ∈ s), infEdist x t) ⊔ ⨆ (y : α) (_ : y ∈ t), infEdist y s =
    (⨆ (y : α) (_ : y ∈ t), infEdist y s) ⊔ ⨆ (x : α) (_ : x ∈ s), infEdist x t
[PROOFSTEP]
apply sup_comm
[GOAL]
ι : Sort u_1
α : Type u
β : Type v
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
x y : α
s t u : Set α
Φ : α → β
r : ℝ≥0∞
H1 : ∀ (x : α), x ∈ s → infEdist x t ≤ r
H2 : ∀ (x : α), x ∈ t → infEdist x s ≤ r
⊢ hausdorffEdist s t ≤ r
[PROOFSTEP]
simp only [hausdorffEdist_def, sup_le_iff, iSup_le_iff]
[GOAL]
ι : Sort u_1
α : Type u
β : Type v
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
x y : α
s t u : Set α
Φ : α → β
r : ℝ≥0∞
H1 : ∀ (x : α), x ∈ s → infEdist x t ≤ r
H2 : ∀ (x : α), x ∈ t → infEdist x s ≤ r
⊢ (∀ (i : α), i ∈ s → infEdist i t ≤ r) ∧ ∀ (i : α), i ∈ t → infEdist i s ≤ r
[PROOFSTEP]
exact ⟨H1, H2⟩
[GOAL]
ι : Sort u_1
α : Type u
β : Type v
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
x y : α
s t u : Set α
Φ : α → β
r : ℝ≥0∞
H1 : ∀ (x : α), x ∈ s → ∃ y, y ∈ t ∧ edist x y ≤ r
H2 : ∀ (x : α), x ∈ t → ∃ y, y ∈ s ∧ edist x y ≤ r
⊢ hausdorffEdist s t ≤ r
[PROOFSTEP]
refine hausdorffEdist_le_of_infEdist (fun x xs ↦ ?_) (fun x xt ↦ ?_)
[GOAL]
case refine_1
ι : Sort u_1
α : Type u
β : Type v
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
x✝ y : α
s t u : Set α
Φ : α → β
r : ℝ≥0∞
H1 : ∀ (x : α), x ∈ s → ∃ y, y ∈ t ∧ edist x y ≤ r
H2 : ∀ (x : α), x ∈ t → ∃ y, y ∈ s ∧ edist x y ≤ r
x : α
xs : x ∈ s
⊢ infEdist x t ≤ r
[PROOFSTEP]
rcases H1 x xs with ⟨y, yt, hy⟩
[GOAL]
case refine_1.intro.intro
ι : Sort u_1
α : Type u
β : Type v
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
x✝ y✝ : α
s t u : Set α
Φ : α → β
r : ℝ≥0∞
H1 : ∀ (x : α), x ∈ s → ∃ y, y ∈ t ∧ edist x y ≤ r
H2 : ∀ (x : α), x ∈ t → ∃ y, y ∈ s ∧ edist x y ≤ r
x : α
xs : x ∈ s
y : α
yt : y ∈ t
hy : edist x y ≤ r
⊢ infEdist x t ≤ r
[PROOFSTEP]
exact le_trans (infEdist_le_edist_of_mem yt) hy
[GOAL]
case refine_2
ι : Sort u_1
α : Type u
β : Type v
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
x✝ y : α
s t u : Set α
Φ : α → β
r : ℝ≥0∞
H1 : ∀ (x : α), x ∈ s → ∃ y, y ∈ t ∧ edist x y ≤ r
H2 : ∀ (x : α), x ∈ t → ∃ y, y ∈ s ∧ edist x y ≤ r
x : α
xt : x ∈ t
⊢ infEdist x s ≤ r
[PROOFSTEP]
rcases H2 x xt with ⟨y, ys, hy⟩
[GOAL]
case refine_2.intro.intro
ι : Sort u_1
α : Type u
β : Type v
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
x✝ y✝ : α
s t u : Set α
Φ : α → β
r : ℝ≥0∞
H1 : ∀ (x : α), x ∈ s → ∃ y, y ∈ t ∧ edist x y ≤ r
H2 : ∀ (x : α), x ∈ t → ∃ y, y ∈ s ∧ edist x y ≤ r
x : α
xt : x ∈ t
y : α
ys : y ∈ s
hy : edist x y ≤ r
⊢ infEdist x s ≤ r
[PROOFSTEP]
exact le_trans (infEdist_le_edist_of_mem ys) hy
[GOAL]
ι : Sort u_1
α : Type u
β : Type v
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
x y : α
s t u : Set α
Φ : α → β
h : x ∈ s
⊢ infEdist x t ≤ hausdorffEdist s t
[PROOFSTEP]
rw [hausdorffEdist_def]
[GOAL]
ι : Sort u_1
α : Type u
β : Type v
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
x y : α
s t u : Set α
Φ : α → β
h : x ∈ s
⊢ infEdist x t ≤ (⨆ (x : α) (_ : x ∈ s), infEdist x t) ⊔ ⨆ (y : α) (_ : y ∈ t), infEdist y s
[PROOFSTEP]
refine le_trans ?_ le_sup_left
[GOAL]
ι : Sort u_1
α : Type u
β : Type v
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
x y : α
s t u : Set α
Φ : α → β
h : x ∈ s
⊢ infEdist x t ≤ ⨆ (x : α) (_ : x ∈ s), infEdist x t
[PROOFSTEP]
exact le_iSup₂ (α := ℝ≥0∞) x h
[GOAL]
ι : Sort u_1
α : Type u
β : Type v
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
x y : α
s t u : Set α
Φ : α → β
ε : ℝ≥0
εpos : 0 < ε
h : infEdist x s + hausdorffEdist s t < ⊤
⊢ infEdist x t ≤ infEdist x s + hausdorffEdist s t + ↑ε
[PROOFSTEP]
have ε0 : (ε / 2 : ℝ≥0∞) ≠ 0 := by simpa [pos_iff_ne_zero] using εpos
[GOAL]
ι : Sort u_1
α : Type u
β : Type v
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
x y : α
s t u : Set α
Φ : α → β
ε : ℝ≥0
εpos : 0 < ε
h : infEdist x s + hausdorffEdist s t < ⊤
⊢ ↑ε / 2 ≠ 0
[PROOFSTEP]
simpa [pos_iff_ne_zero] using εpos
[GOAL]
ι : Sort u_1
α : Type u
β : Type v
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
x y : α
s t u : Set α
Φ : α → β
ε : ℝ≥0
εpos : 0 < ε
h : infEdist x s + hausdorffEdist s t < ⊤
ε0 : ↑ε / 2 ≠ 0
⊢ infEdist x t ≤ infEdist x s + hausdorffEdist s t + ↑ε
[PROOFSTEP]
have : infEdist x s < infEdist x s + ε / 2 := ENNReal.lt_add_right (ENNReal.add_lt_top.1 h).1.ne ε0
[GOAL]
ι : Sort u_1
α : Type u
β : Type v
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
x y : α
s t u : Set α
Φ : α → β
ε : ℝ≥0
εpos : 0 < ε
h : infEdist x s + hausdorffEdist s t < ⊤
ε0 : ↑ε / 2 ≠ 0
this : infEdist x s < infEdist x s + ↑ε / 2
⊢ infEdist x t ≤ infEdist x s + hausdorffEdist s t + ↑ε
[PROOFSTEP]
rcases infEdist_lt_iff.mp this with
  ⟨y, ys, dxy⟩
    -- y : α, ys : y ∈ s, dxy : edist x y < infEdist x s + ↑ε / 2
[GOAL]
case intro.intro
ι : Sort u_1
α : Type u
β : Type v
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
x y✝ : α
s t u : Set α
Φ : α → β
ε : ℝ≥0
εpos : 0 < ε
h : infEdist x s + hausdorffEdist s t < ⊤
ε0 : ↑ε / 2 ≠ 0
this : infEdist x s < infEdist x s + ↑ε / 2
y : α
ys : y ∈ s
dxy : edist x y < infEdist x s + ↑ε / 2
⊢ infEdist x t ≤ infEdist x s + hausdorffEdist s t + ↑ε
[PROOFSTEP]
have : hausdorffEdist s t < hausdorffEdist s t + ε / 2 := ENNReal.lt_add_right (ENNReal.add_lt_top.1 h).2.ne ε0
[GOAL]
case intro.intro
ι : Sort u_1
α : Type u
β : Type v
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
x y✝ : α
s t u : Set α
Φ : α → β
ε : ℝ≥0
εpos : 0 < ε
h : infEdist x s + hausdorffEdist s t < ⊤
ε0 : ↑ε / 2 ≠ 0
this✝ : infEdist x s < infEdist x s + ↑ε / 2
y : α
ys : y ∈ s
dxy : edist x y < infEdist x s + ↑ε / 2
this : hausdorffEdist s t < hausdorffEdist s t + ↑ε / 2
⊢ infEdist x t ≤ infEdist x s + hausdorffEdist s t + ↑ε
[PROOFSTEP]
rcases exists_edist_lt_of_hausdorffEdist_lt ys this with
  ⟨z, zt, dyz⟩
    -- z : α, zt : z ∈ t, dyz : edist y z < Hausdorff_edist s t + ↑ε / 2
[GOAL]
case intro.intro.intro.intro
ι : Sort u_1
α : Type u
β : Type v
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
x y✝ : α
s t u : Set α
Φ : α → β
ε : ℝ≥0
εpos : 0 < ε
h : infEdist x s + hausdorffEdist s t < ⊤
ε0 : ↑ε / 2 ≠ 0
this✝ : infEdist x s < infEdist x s + ↑ε / 2
y : α
ys : y ∈ s
dxy : edist x y < infEdist x s + ↑ε / 2
this : hausdorffEdist s t < hausdorffEdist s t + ↑ε / 2
z : α
zt : z ∈ t
dyz : edist y z < hausdorffEdist s t + ↑ε / 2
⊢ infEdist x t ≤ infEdist x s + hausdorffEdist s t + ↑ε
[PROOFSTEP]
calc
  infEdist x t ≤ edist x z := infEdist_le_edist_of_mem zt
  _ ≤ edist x y + edist y z := (edist_triangle _ _ _)
  _ ≤ infEdist x s + ε / 2 + (hausdorffEdist s t + ε / 2) := (add_le_add dxy.le dyz.le)
  _ = infEdist x s + hausdorffEdist s t + ε := by simp [ENNReal.add_halves, add_comm, add_left_comm]
[GOAL]
ι : Sort u_1
α : Type u
β : Type v
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
x y✝ : α
s t u : Set α
Φ : α → β
ε : ℝ≥0
εpos : 0 < ε
h : infEdist x s + hausdorffEdist s t < ⊤
ε0 : ↑ε / 2 ≠ 0
this✝ : infEdist x s < infEdist x s + ↑ε / 2
y : α
ys : y ∈ s
dxy : edist x y < infEdist x s + ↑ε / 2
this : hausdorffEdist s t < hausdorffEdist s t + ↑ε / 2
z : α
zt : z ∈ t
dyz : edist y z < hausdorffEdist s t + ↑ε / 2
⊢ infEdist x s + ↑ε / 2 + (hausdorffEdist s t + ↑ε / 2) = infEdist x s + hausdorffEdist s t + ↑ε
[PROOFSTEP]
simp [ENNReal.add_halves, add_comm, add_left_comm]
[GOAL]
ι : Sort u_1
α : Type u
β : Type v
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
x y : α
s t u : Set α
Φ : α → β
h : Isometry Φ
⊢ hausdorffEdist (Φ '' s) (Φ '' t) = hausdorffEdist s t
[PROOFSTEP]
simp only [hausdorffEdist_def, iSup_image, infEdist_image h]
[GOAL]
ι : Sort u_1
α : Type u
β : Type v
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
x y : α
s t u : Set α
Φ : α → β
hs : Set.Nonempty s
ht : Set.Nonempty t
⊢ hausdorffEdist s t ≤ diam (s ∪ t)
[PROOFSTEP]
rcases hs with ⟨x, xs⟩
[GOAL]
case intro
ι : Sort u_1
α : Type u
β : Type v
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
x✝ y : α
s t u : Set α
Φ : α → β
ht : Set.Nonempty t
x : α
xs : x ∈ s
⊢ hausdorffEdist s t ≤ diam (s ∪ t)
[PROOFSTEP]
rcases ht with ⟨y, yt⟩
[GOAL]
case intro.intro
ι : Sort u_1
α : Type u
β : Type v
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
x✝ y✝ : α
s t u : Set α
Φ : α → β
x : α
xs : x ∈ s
y : α
yt : y ∈ t
⊢ hausdorffEdist s t ≤ diam (s ∪ t)
[PROOFSTEP]
refine' hausdorffEdist_le_of_mem_edist _ _
[GOAL]
case intro.intro.refine'_1
ι : Sort u_1
α : Type u
β : Type v
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
x✝ y✝ : α
s t u : Set α
Φ : α → β
x : α
xs : x ∈ s
y : α
yt : y ∈ t
⊢ ∀ (x : α), x ∈ s → ∃ y, y ∈ t ∧ edist x y ≤ diam (s ∪ t)
[PROOFSTEP]
intro z hz
[GOAL]
case intro.intro.refine'_1
ι : Sort u_1
α : Type u
β : Type v
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
x✝ y✝ : α
s t u : Set α
Φ : α → β
x : α
xs : x ∈ s
y : α
yt : y ∈ t
z : α
hz : z ∈ s
⊢ ∃ y, y ∈ t ∧ edist z y ≤ diam (s ∪ t)
[PROOFSTEP]
exact ⟨y, yt, edist_le_diam_of_mem (subset_union_left _ _ hz) (subset_union_right _ _ yt)⟩
[GOAL]
case intro.intro.refine'_2
ι : Sort u_1
α : Type u
β : Type v
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
x✝ y✝ : α
s t u : Set α
Φ : α → β
x : α
xs : x ∈ s
y : α
yt : y ∈ t
⊢ ∀ (x : α), x ∈ t → ∃ y, y ∈ s ∧ edist x y ≤ diam (s ∪ t)
[PROOFSTEP]
intro z hz
[GOAL]
case intro.intro.refine'_2
ι : Sort u_1
α : Type u
β : Type v
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
x✝ y✝ : α
s t u : Set α
Φ : α → β
x : α
xs : x ∈ s
y : α
yt : y ∈ t
z : α
hz : z ∈ t
⊢ ∃ y, y ∈ s ∧ edist z y ≤ diam (s ∪ t)
[PROOFSTEP]
exact ⟨x, xs, edist_le_diam_of_mem (subset_union_right _ _ hz) (subset_union_left _ _ xs)⟩
[GOAL]
ι : Sort u_1
α : Type u
β : Type v
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
x y : α
s t u : Set α
Φ : α → β
⊢ hausdorffEdist s u ≤ hausdorffEdist s t + hausdorffEdist t u
[PROOFSTEP]
rw [hausdorffEdist_def]
[GOAL]
ι : Sort u_1
α : Type u
β : Type v
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
x y : α
s t u : Set α
Φ : α → β
⊢ (⨆ (x : α) (_ : x ∈ s), infEdist x u) ⊔ ⨆ (y : α) (_ : y ∈ u), infEdist y s ≤ hausdorffEdist s t + hausdorffEdist t u
[PROOFSTEP]
simp only [sup_le_iff, iSup_le_iff]
[GOAL]
ι : Sort u_1
α : Type u
β : Type v
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
x y : α
s t u : Set α
Φ : α → β
⊢ (∀ (i : α), i ∈ s → infEdist i u ≤ hausdorffEdist s t + hausdorffEdist t u) ∧
    ∀ (i : α), i ∈ u → infEdist i s ≤ hausdorffEdist s t + hausdorffEdist t u
[PROOFSTEP]
constructor
[GOAL]
case left
ι : Sort u_1
α : Type u
β : Type v
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
x y : α
s t u : Set α
Φ : α → β
⊢ ∀ (i : α), i ∈ s → infEdist i u ≤ hausdorffEdist s t + hausdorffEdist t u
[PROOFSTEP]
show ∀ x ∈ s, infEdist x u ≤ hausdorffEdist s t + hausdorffEdist t u
[GOAL]
case left
ι : Sort u_1
α : Type u
β : Type v
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
x y : α
s t u : Set α
Φ : α → β
⊢ ∀ (x : α), x ∈ s → infEdist x u ≤ hausdorffEdist s t + hausdorffEdist t u
[PROOFSTEP]
exact fun x xs =>
  calc
    infEdist x u ≤ infEdist x t + hausdorffEdist t u := infEdist_le_infEdist_add_hausdorffEdist
    _ ≤ hausdorffEdist s t + hausdorffEdist t u := add_le_add_right (infEdist_le_hausdorffEdist_of_mem xs) _
[GOAL]
case right
ι : Sort u_1
α : Type u
β : Type v
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
x y : α
s t u : Set α
Φ : α → β
⊢ ∀ (i : α), i ∈ u → infEdist i s ≤ hausdorffEdist s t + hausdorffEdist t u
[PROOFSTEP]
show ∀ x ∈ u, infEdist x s ≤ hausdorffEdist s t + hausdorffEdist t u
[GOAL]
case right
ι : Sort u_1
α : Type u
β : Type v
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
x y : α
s t u : Set α
Φ : α → β
⊢ ∀ (x : α), x ∈ u → infEdist x s ≤ hausdorffEdist s t + hausdorffEdist t u
[PROOFSTEP]
exact fun x xu =>
  calc
    infEdist x s ≤ infEdist x t + hausdorffEdist t s := infEdist_le_infEdist_add_hausdorffEdist
    _ ≤ hausdorffEdist u t + hausdorffEdist t s := (add_le_add_right (infEdist_le_hausdorffEdist_of_mem xu) _)
    _ = hausdorffEdist s t + hausdorffEdist t u := by simp [hausdorffEdist_comm, add_comm]
[GOAL]
ι : Sort u_1
α : Type u
β : Type v
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
x✝ y : α
s t u : Set α
Φ : α → β
x : α
xu : x ∈ u
⊢ hausdorffEdist u t + hausdorffEdist t s = hausdorffEdist s t + hausdorffEdist t u
[PROOFSTEP]
simp [hausdorffEdist_comm, add_comm]
[GOAL]
ι : Sort u_1
α : Type u
β : Type v
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
x y : α
s t u : Set α
Φ : α → β
⊢ hausdorffEdist s t = 0 ↔ closure s = closure t
[PROOFSTEP]
simp only [hausdorffEdist_def, ENNReal.sup_eq_zero, ENNReal.iSup_eq_zero, ← subset_def, ← mem_closure_iff_infEdist_zero,
  subset_antisymm_iff, isClosed_closure.closure_subset_iff]
[GOAL]
ι : Sort u_1
α : Type u
β : Type v
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
x y : α
s t u : Set α
Φ : α → β
⊢ hausdorffEdist s (closure s) = 0
[PROOFSTEP]
rw [hausdorffEdist_zero_iff_closure_eq_closure, closure_closure]
[GOAL]
ι : Sort u_1
α : Type u
β : Type v
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
x y : α
s t u : Set α
Φ : α → β
⊢ hausdorffEdist (closure s) t = hausdorffEdist s t
[PROOFSTEP]
refine' le_antisymm _ _
[GOAL]
case refine'_1
ι : Sort u_1
α : Type u
β : Type v
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
x y : α
s t u : Set α
Φ : α → β
⊢ hausdorffEdist (closure s) t ≤ hausdorffEdist s t
[PROOFSTEP]
calc
  _ ≤ hausdorffEdist (closure s) s + hausdorffEdist s t := hausdorffEdist_triangle
  _ = hausdorffEdist s t := by simp [hausdorffEdist_comm]
[GOAL]
ι : Sort u_1
α : Type u
β : Type v
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
x y : α
s t u : Set α
Φ : α → β
⊢ hausdorffEdist (closure s) s + hausdorffEdist s t = hausdorffEdist s t
[PROOFSTEP]
simp [hausdorffEdist_comm]
[GOAL]
case refine'_2
ι : Sort u_1
α : Type u
β : Type v
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
x y : α
s t u : Set α
Φ : α → β
⊢ hausdorffEdist s t ≤ hausdorffEdist (closure s) t
[PROOFSTEP]
calc
  _ ≤ hausdorffEdist s (closure s) + hausdorffEdist (closure s) t := hausdorffEdist_triangle
  _ = hausdorffEdist (closure s) t := by simp
[GOAL]
ι : Sort u_1
α : Type u
β : Type v
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
x y : α
s t u : Set α
Φ : α → β
⊢ hausdorffEdist s (closure s) + hausdorffEdist (closure s) t = hausdorffEdist (closure s) t
[PROOFSTEP]
simp
[GOAL]
ι : Sort u_1
α : Type u
β : Type v
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
x y : α
s t u : Set α
Φ : α → β
⊢ hausdorffEdist s (closure t) = hausdorffEdist s t
[PROOFSTEP]
simp [@hausdorffEdist_comm _ _ s _]
[GOAL]
ι : Sort u_1
α : Type u
β : Type v
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
x y : α
s t u : Set α
Φ : α → β
⊢ hausdorffEdist (closure s) (closure t) = hausdorffEdist s t
[PROOFSTEP]
simp
[GOAL]
ι : Sort u_1
α : Type u
β : Type v
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
x y : α
s t u : Set α
Φ : α → β
hs : IsClosed s
ht : IsClosed t
⊢ hausdorffEdist s t = 0 ↔ s = t
[PROOFSTEP]
rw [hausdorffEdist_zero_iff_closure_eq_closure, hs.closure_eq, ht.closure_eq]
[GOAL]
ι : Sort u_1
α : Type u
β : Type v
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
x y : α
s t u : Set α
Φ : α → β
ne : Set.Nonempty s
⊢ hausdorffEdist s ∅ = ⊤
[PROOFSTEP]
rcases ne with ⟨x, xs⟩
[GOAL]
case intro
ι : Sort u_1
α : Type u
β : Type v
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
x✝ y : α
s t u : Set α
Φ : α → β
x : α
xs : x ∈ s
⊢ hausdorffEdist s ∅ = ⊤
[PROOFSTEP]
have : infEdist x ∅ ≤ hausdorffEdist s ∅ := infEdist_le_hausdorffEdist_of_mem xs
[GOAL]
case intro
ι : Sort u_1
α : Type u
β : Type v
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
x✝ y : α
s t u : Set α
Φ : α → β
x : α
xs : x ∈ s
this : infEdist x ∅ ≤ hausdorffEdist s ∅
⊢ hausdorffEdist s ∅ = ⊤
[PROOFSTEP]
simpa using this
[GOAL]
ι : Sort u_1
α : Type u
β : Type v
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
x y : α
s t u : Set α
Φ : α → β
fin : hausdorffEdist s t ≠ ⊤
⊢ s = ∅ ∧ t = ∅ ∨ Set.Nonempty s ∧ Set.Nonempty t
[PROOFSTEP]
cases' s.eq_empty_or_nonempty with hs hs
[GOAL]
case inl
ι : Sort u_1
α : Type u
β : Type v
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
x y : α
s t u : Set α
Φ : α → β
fin : hausdorffEdist s t ≠ ⊤
hs : s = ∅
⊢ s = ∅ ∧ t = ∅ ∨ Set.Nonempty s ∧ Set.Nonempty t
[PROOFSTEP]
cases' t.eq_empty_or_nonempty with ht ht
[GOAL]
case inl.inl
ι : Sort u_1
α : Type u
β : Type v
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
x y : α
s t u : Set α
Φ : α → β
fin : hausdorffEdist s t ≠ ⊤
hs : s = ∅
ht : t = ∅
⊢ s = ∅ ∧ t = ∅ ∨ Set.Nonempty s ∧ Set.Nonempty t
[PROOFSTEP]
exact Or.inl ⟨hs, ht⟩
[GOAL]
case inl.inr
ι : Sort u_1
α : Type u
β : Type v
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
x y : α
s t u : Set α
Φ : α → β
fin : hausdorffEdist s t ≠ ⊤
hs : s = ∅
ht : Set.Nonempty t
⊢ s = ∅ ∧ t = ∅ ∨ Set.Nonempty s ∧ Set.Nonempty t
[PROOFSTEP]
rw [hausdorffEdist_comm] at fin 
[GOAL]
case inl.inr
ι : Sort u_1
α : Type u
β : Type v
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
x y : α
s t u : Set α
Φ : α → β
fin : hausdorffEdist t s ≠ ⊤
hs : s = ∅
ht : Set.Nonempty t
⊢ s = ∅ ∧ t = ∅ ∨ Set.Nonempty s ∧ Set.Nonempty t
[PROOFSTEP]
exact Or.inr ⟨nonempty_of_hausdorffEdist_ne_top ht fin, ht⟩
[GOAL]
case inr
ι : Sort u_1
α : Type u
β : Type v
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
x y : α
s t u : Set α
Φ : α → β
fin : hausdorffEdist s t ≠ ⊤
hs : Set.Nonempty s
⊢ s = ∅ ∧ t = ∅ ∨ Set.Nonempty s ∧ Set.Nonempty t
[PROOFSTEP]
exact Or.inr ⟨hs, nonempty_of_hausdorffEdist_ne_top hs fin⟩
[GOAL]
ι : Sort u_1
α : Type u
β : Type v
inst✝¹ : PseudoMetricSpace α
inst✝ : PseudoMetricSpace β
s t u : Set α
x y : α
Φ : α → β
⊢ infDist x s = ⨅ (y : ↑s), dist x ↑y
[PROOFSTEP]
rw [infDist, infEdist, iInf_subtype', ENNReal.toReal_iInf]
[GOAL]
ι : Sort u_1
α : Type u
β : Type v
inst✝¹ : PseudoMetricSpace α
inst✝ : PseudoMetricSpace β
s t u : Set α
x y : α
Φ : α → β
⊢ ⨅ (i : { y // y ∈ s }), ENNReal.toReal (edist x ↑i) = ⨅ (y : ↑s), dist x ↑y
[PROOFSTEP]
simp only [dist_edist]
[GOAL]
ι : Sort u_1
α : Type u
β : Type v
inst✝¹ : PseudoMetricSpace α
inst✝ : PseudoMetricSpace β
s t u : Set α
x y : α
Φ : α → β
⊢ ∀ (i : { y // y ∈ s }), edist x ↑i ≠ ⊤
[PROOFSTEP]
exact fun _ ↦ edist_ne_top _ _
[GOAL]
ι : Sort u_1
α : Type u
β : Type v
inst✝¹ : PseudoMetricSpace α
inst✝ : PseudoMetricSpace β
s t u : Set α
x y : α
Φ : α → β
⊢ infDist x ∅ = 0
[PROOFSTEP]
simp [infDist]
[GOAL]
ι : Sort u_1
α : Type u
β : Type v
inst✝¹ : PseudoMetricSpace α
inst✝ : PseudoMetricSpace β
s t u : Set α
x y : α
Φ : α → β
h : Set.Nonempty s
⊢ infEdist x s ≠ ⊤
[PROOFSTEP]
rcases h with ⟨y, hy⟩
[GOAL]
case intro
ι : Sort u_1
α : Type u
β : Type v
inst✝¹ : PseudoMetricSpace α
inst✝ : PseudoMetricSpace β
s t u : Set α
x y✝ : α
Φ : α → β
y : α
hy : y ∈ s
⊢ infEdist x s ≠ ⊤
[PROOFSTEP]
exact ne_top_of_le_ne_top (edist_ne_top _ _) (infEdist_le_edist_of_mem hy)
[GOAL]
ι : Sort u_1
α : Type u
β : Type v
inst✝¹ : PseudoMetricSpace α
inst✝ : PseudoMetricSpace β
s t u : Set α
x y : α
Φ : α → β
⊢ infEdist x s = ⊤ ↔ s = ∅
[PROOFSTEP]
rcases s.eq_empty_or_nonempty with rfl | hs
[GOAL]
case inl
ι : Sort u_1
α : Type u
β : Type v
inst✝¹ : PseudoMetricSpace α
inst✝ : PseudoMetricSpace β
t u : Set α
x y : α
Φ : α → β
⊢ infEdist x ∅ = ⊤ ↔ ∅ = ∅
[PROOFSTEP]
simp [*, Nonempty.ne_empty, infEdist_ne_top]
[GOAL]
case inr
ι : Sort u_1
α : Type u
β : Type v
inst✝¹ : PseudoMetricSpace α
inst✝ : PseudoMetricSpace β
s t u : Set α
x y : α
Φ : α → β
hs : Set.Nonempty s
⊢ infEdist x s = ⊤ ↔ s = ∅
[PROOFSTEP]
simp [*, Nonempty.ne_empty, infEdist_ne_top]
[GOAL]
ι : Sort u_1
α : Type u
β : Type v
inst✝¹ : PseudoMetricSpace α
inst✝ : PseudoMetricSpace β
s t u : Set α
x y : α
Φ : α → β
h : x ∈ s
⊢ infDist x s = 0
[PROOFSTEP]
simp [infEdist_zero_of_mem h, infDist]
[GOAL]
ι : Sort u_1
α : Type u
β : Type v
inst✝¹ : PseudoMetricSpace α
inst✝ : PseudoMetricSpace β
s t u : Set α
x y : α
Φ : α → β
⊢ infDist x {y} = dist x y
[PROOFSTEP]
simp [infDist, dist_edist]
[GOAL]
ι : Sort u_1
α : Type u
β : Type v
inst✝¹ : PseudoMetricSpace α
inst✝ : PseudoMetricSpace β
s t u : Set α
x y : α
Φ : α → β
h : y ∈ s
⊢ infDist x s ≤ dist x y
[PROOFSTEP]
rw [dist_edist, infDist]
[GOAL]
ι : Sort u_1
α : Type u
β : Type v
inst✝¹ : PseudoMetricSpace α
inst✝ : PseudoMetricSpace β
s t u : Set α
x y : α
Φ : α → β
h : y ∈ s
⊢ ENNReal.toReal (infEdist x s) ≤ ENNReal.toReal (edist x y)
[PROOFSTEP]
exact ENNReal.toReal_mono (edist_ne_top _ _) (infEdist_le_edist_of_mem h)
[GOAL]
ι : Sort u_1
α : Type u
β : Type v
inst✝¹ : PseudoMetricSpace α
inst✝ : PseudoMetricSpace β
s t u : Set α
x y : α
Φ : α → β
r : ℝ
hs : Set.Nonempty s
⊢ infDist x s < r ↔ ∃ y, y ∈ s ∧ dist x y < r
[PROOFSTEP]
simp_rw [infDist, ← ENNReal.lt_ofReal_iff_toReal_lt (infEdist_ne_top hs), infEdist_lt_iff,
  ENNReal.lt_ofReal_iff_toReal_lt (edist_ne_top _ _), ← dist_edist]
[GOAL]
ι : Sort u_1
α : Type u
β : Type v
inst✝¹ : PseudoMetricSpace α
inst✝ : PseudoMetricSpace β
s t u : Set α
x y : α
Φ : α → β
⊢ infDist x s ≤ infDist y s + dist x y
[PROOFSTEP]
rw [infDist, infDist, dist_edist]
[GOAL]
ι : Sort u_1
α : Type u
β : Type v
inst✝¹ : PseudoMetricSpace α
inst✝ : PseudoMetricSpace β
s t u : Set α
x y : α
Φ : α → β
⊢ ENNReal.toReal (infEdist x s) ≤ ENNReal.toReal (infEdist y s) + ENNReal.toReal (edist x y)
[PROOFSTEP]
refine ENNReal.toReal_le_add' infEdist_le_infEdist_add_edist ?_ (flip absurd (edist_ne_top _ _))
[GOAL]
ι : Sort u_1
α : Type u
β : Type v
inst✝¹ : PseudoMetricSpace α
inst✝ : PseudoMetricSpace β
s t u : Set α
x y : α
Φ : α → β
⊢ infEdist y s = ⊤ → infEdist x s = ⊤
[PROOFSTEP]
simp only [infEdist_eq_top_iff, imp_self]
[GOAL]
ι : Sort u_1
α : Type u
β : Type v
inst✝¹ : PseudoMetricSpace α
inst✝ : PseudoMetricSpace β
s t u : Set α
x y : α
Φ : α → β
hs : Bounded s
hy : y ∈ s
⊢ dist x y ≤ infDist x s + diam s
[PROOFSTEP]
rw [infDist, diam, dist_edist]
[GOAL]
ι : Sort u_1
α : Type u
β : Type v
inst✝¹ : PseudoMetricSpace α
inst✝ : PseudoMetricSpace β
s t u : Set α
x y : α
Φ : α → β
hs : Bounded s
hy : y ∈ s
⊢ ENNReal.toReal (edist x y) ≤ ENNReal.toReal (infEdist x s) + ENNReal.toReal (EMetric.diam s)
[PROOFSTEP]
exact toReal_le_add (edist_le_infEdist_add_ediam hy) (infEdist_ne_top ⟨y, hy⟩) hs.ediam_ne_top
[GOAL]
ι : Sort u_1
α : Type u
β : Type v
inst✝¹ : PseudoMetricSpace α
inst✝ : PseudoMetricSpace β
s t u : Set α
x y : α
Φ : α → β
⊢ infDist x (closure s) = infDist x s
[PROOFSTEP]
simp [infDist, infEdist_closure]
[GOAL]
ι : Sort u_1
α : Type u
β : Type v
inst✝¹ : PseudoMetricSpace α
inst✝ : PseudoMetricSpace β
s t u : Set α
x y : α
Φ : α → β
hx : x ∈ closure s
⊢ infDist x s = 0
[PROOFSTEP]
rw [← infDist_closure]
[GOAL]
ι : Sort u_1
α : Type u
β : Type v
inst✝¹ : PseudoMetricSpace α
inst✝ : PseudoMetricSpace β
s t u : Set α
x y : α
Φ : α → β
hx : x ∈ closure s
⊢ infDist x (closure s) = 0
[PROOFSTEP]
exact infDist_zero_of_mem hx
[GOAL]
ι : Sort u_1
α : Type u
β : Type v
inst✝¹ : PseudoMetricSpace α
inst✝ : PseudoMetricSpace β
s t u : Set α
x y : α
Φ : α → β
h : Set.Nonempty s
⊢ x ∈ closure s ↔ infDist x s = 0
[PROOFSTEP]
simp [mem_closure_iff_infEdist_zero, infDist, ENNReal.toReal_eq_zero_iff, infEdist_ne_top h]
[GOAL]
ι : Sort u_1
α : Type u
β : Type v
inst✝¹ : PseudoMetricSpace α
inst✝ : PseudoMetricSpace β
s t u : Set α
x y : α
Φ : α → β
h : IsClosed s
hs : Set.Nonempty s
⊢ x ∈ s ↔ infDist x s = 0
[PROOFSTEP]
rw [← mem_closure_iff_infDist_zero hs, h.closure_eq]
[GOAL]
ι : Sort u_1
α : Type u
β : Type v
inst✝¹ : PseudoMetricSpace α
inst✝ : PseudoMetricSpace β
s t u : Set α
x y : α
Φ : α → β
h : IsClosed s
hs : Set.Nonempty s
⊢ ¬x ∈ s ↔ 0 < infDist x s
[PROOFSTEP]
simp [h.mem_iff_infDist_zero hs, infDist_nonneg.gt_iff_ne]
[GOAL]
ι : Sort u_1
α : Type u
β : Type v
inst✝¹ : PseudoMetricSpace α
inst✝ : PseudoMetricSpace β
s t u : Set α
x y : α
Φ : α → β
h : ¬x ∈ closure s
⊢ ContinuousAt (fun x => (infDist x s)⁻¹) x
[PROOFSTEP]
rcases s.eq_empty_or_nonempty with (rfl | hs)
[GOAL]
case inl
ι : Sort u_1
α : Type u
β : Type v
inst✝¹ : PseudoMetricSpace α
inst✝ : PseudoMetricSpace β
t u : Set α
x y : α
Φ : α → β
h : ¬x ∈ closure ∅
⊢ ContinuousAt (fun x => (infDist x ∅)⁻¹) x
[PROOFSTEP]
simp only [infDist_empty, continuousAt_const]
[GOAL]
case inr
ι : Sort u_1
α : Type u
β : Type v
inst✝¹ : PseudoMetricSpace α
inst✝ : PseudoMetricSpace β
s t u : Set α
x y : α
Φ : α → β
h : ¬x ∈ closure s
hs : Set.Nonempty s
⊢ ContinuousAt (fun x => (infDist x s)⁻¹) x
[PROOFSTEP]
refine (continuous_infDist_pt s).continuousAt.inv₀ ?_
[GOAL]
case inr
ι : Sort u_1
α : Type u
β : Type v
inst✝¹ : PseudoMetricSpace α
inst✝ : PseudoMetricSpace β
s t u : Set α
x y : α
Φ : α → β
h : ¬x ∈ closure s
hs : Set.Nonempty s
⊢ infDist x s ≠ 0
[PROOFSTEP]
rwa [Ne.def, ← mem_closure_iff_infDist_zero hs]
[GOAL]
ι : Sort u_1
α : Type u
β : Type v
inst✝¹ : PseudoMetricSpace α
inst✝ : PseudoMetricSpace β
s t u : Set α
x y : α
Φ : α → β
hΦ : Isometry Φ
⊢ infDist (Φ x) (Φ '' t) = infDist x t
[PROOFSTEP]
simp [infDist, infEdist_image hΦ]
[GOAL]
ι : Sort u_1
α : Type u
β : Type v
inst✝¹ : PseudoMetricSpace α
inst✝ : PseudoMetricSpace β
s t u : Set α
x y : α
Φ : α → β
h : y ∈ s
⊢ infDist x (s ∩ closedBall x (dist y x)) = infDist x s
[PROOFSTEP]
replace h : y ∈ s ∩ closedBall x (dist y x) := ⟨h, mem_closedBall.2 le_rfl⟩
[GOAL]
ι : Sort u_1
α : Type u
β : Type v
inst✝¹ : PseudoMetricSpace α
inst✝ : PseudoMetricSpace β
s t u : Set α
x y : α
Φ : α → β
h : y ∈ s ∩ closedBall x (dist y x)
⊢ infDist x (s ∩ closedBall x (dist y x)) = infDist x s
[PROOFSTEP]
refine le_antisymm ?_ (infDist_le_infDist_of_subset (inter_subset_left _ _) ⟨y, h⟩)
[GOAL]
ι : Sort u_1
α : Type u
β : Type v
inst✝¹ : PseudoMetricSpace α
inst✝ : PseudoMetricSpace β
s t u : Set α
x y : α
Φ : α → β
h : y ∈ s ∩ closedBall x (dist y x)
⊢ infDist x (s ∩ closedBall x (dist y x)) ≤ infDist x s
[PROOFSTEP]
refine' not_lt.1 fun hlt => _
[GOAL]
ι : Sort u_1
α : Type u
β : Type v
inst✝¹ : PseudoMetricSpace α
inst✝ : PseudoMetricSpace β
s t u : Set α
x y : α
Φ : α → β
h : y ∈ s ∩ closedBall x (dist y x)
hlt : infDist x s < infDist x (s ∩ closedBall x (dist y x))
⊢ False
[PROOFSTEP]
rcases(infDist_lt_iff ⟨y, h.1⟩).mp hlt with ⟨z, hzs, hz⟩
[GOAL]
case intro.intro
ι : Sort u_1
α : Type u
β : Type v
inst✝¹ : PseudoMetricSpace α
inst✝ : PseudoMetricSpace β
s t u : Set α
x y : α
Φ : α → β
h : y ∈ s ∩ closedBall x (dist y x)
hlt : infDist x s < infDist x (s ∩ closedBall x (dist y x))
z : α
hzs : z ∈ s
hz : dist x z < infDist x (s ∩ closedBall x (dist y x))
⊢ False
[PROOFSTEP]
cases' le_or_lt (dist z x) (dist y x) with hle hlt
[GOAL]
case intro.intro.inl
ι : Sort u_1
α : Type u
β : Type v
inst✝¹ : PseudoMetricSpace α
inst✝ : PseudoMetricSpace β
s t u : Set α
x y : α
Φ : α → β
h : y ∈ s ∩ closedBall x (dist y x)
hlt : infDist x s < infDist x (s ∩ closedBall x (dist y x))
z : α
hzs : z ∈ s
hz : dist x z < infDist x (s ∩ closedBall x (dist y x))
hle : dist z x ≤ dist y x
⊢ False
[PROOFSTEP]
exact hz.not_le (infDist_le_dist_of_mem ⟨hzs, hle⟩)
[GOAL]
case intro.intro.inr
ι : Sort u_1
α : Type u
β : Type v
inst✝¹ : PseudoMetricSpace α
inst✝ : PseudoMetricSpace β
s t u : Set α
x y : α
Φ : α → β
h : y ∈ s ∩ closedBall x (dist y x)
hlt✝ : infDist x s < infDist x (s ∩ closedBall x (dist y x))
z : α
hzs : z ∈ s
hz : dist x z < infDist x (s ∩ closedBall x (dist y x))
hlt : dist y x < dist z x
⊢ False
[PROOFSTEP]
rw [dist_comm z, dist_comm y] at hlt 
[GOAL]
case intro.intro.inr
ι : Sort u_1
α : Type u
β : Type v
inst✝¹ : PseudoMetricSpace α
inst✝ : PseudoMetricSpace β
s t u : Set α
x y : α
Φ : α → β
h : y ∈ s ∩ closedBall x (dist y x)
hlt✝ : infDist x s < infDist x (s ∩ closedBall x (dist y x))
z : α
hzs : z ∈ s
hz : dist x z < infDist x (s ∩ closedBall x (dist y x))
hlt : dist x y < dist x z
⊢ False
[PROOFSTEP]
exact (hlt.trans hz).not_le (infDist_le_dist_of_mem h)
[GOAL]
ι : Sort u_1
α : Type u
β : Type v
inst✝¹ : PseudoMetricSpace α
inst✝ : PseudoMetricSpace β
s t u : Set α
x✝ y✝ : α
Φ : α → β
h : IsCompact s
hne : Set.Nonempty s
x y : α
hys : y ∈ s
hy : infEdist x s = edist x y
⊢ infDist x s = dist x y
[PROOFSTEP]
rw [infDist, dist_edist, hy]
[GOAL]
ι : Sort u_1
α : Type u
β : Type v
inst✝² : PseudoMetricSpace α
inst✝¹ : PseudoMetricSpace β
s t u : Set α
x✝ y : α
Φ : α → β
inst✝ : ProperSpace α
h : IsClosed s
hne : Set.Nonempty s
x : α
⊢ ∃ y, y ∈ s ∧ infDist x s = dist x y
[PROOFSTEP]
rcases hne with ⟨z, hz⟩
[GOAL]
case intro
ι : Sort u_1
α : Type u
β : Type v
inst✝² : PseudoMetricSpace α
inst✝¹ : PseudoMetricSpace β
s t u : Set α
x✝ y : α
Φ : α → β
inst✝ : ProperSpace α
h : IsClosed s
x z : α
hz : z ∈ s
⊢ ∃ y, y ∈ s ∧ infDist x s = dist x y
[PROOFSTEP]
rw [← infDist_inter_closedBall_of_mem hz]
[GOAL]
case intro
ι : Sort u_1
α : Type u
β : Type v
inst✝² : PseudoMetricSpace α
inst✝¹ : PseudoMetricSpace β
s t u : Set α
x✝ y : α
Φ : α → β
inst✝ : ProperSpace α
h : IsClosed s
x z : α
hz : z ∈ s
⊢ ∃ y, y ∈ s ∧ infDist x (s ∩ closedBall x (dist z x)) = dist x y
[PROOFSTEP]
set t := s ∩ closedBall x (dist z x)
[GOAL]
case intro
ι : Sort u_1
α : Type u
β : Type v
inst✝² : PseudoMetricSpace α
inst✝¹ : PseudoMetricSpace β
s t✝ u : Set α
x✝ y : α
Φ : α → β
inst✝ : ProperSpace α
h : IsClosed s
x z : α
hz : z ∈ s
t : Set α := s ∩ closedBall x (dist z x)
⊢ ∃ y, y ∈ s ∧ infDist x t = dist x y
[PROOFSTEP]
have htc : IsCompact t := (isCompact_closedBall x (dist z x)).inter_left h
[GOAL]
case intro
ι : Sort u_1
α : Type u
β : Type v
inst✝² : PseudoMetricSpace α
inst✝¹ : PseudoMetricSpace β
s t✝ u : Set α
x✝ y : α
Φ : α → β
inst✝ : ProperSpace α
h : IsClosed s
x z : α
hz : z ∈ s
t : Set α := s ∩ closedBall x (dist z x)
htc : IsCompact t
⊢ ∃ y, y ∈ s ∧ infDist x t = dist x y
[PROOFSTEP]
have htne : t.Nonempty := ⟨z, hz, mem_closedBall.2 le_rfl⟩
[GOAL]
case intro
ι : Sort u_1
α : Type u
β : Type v
inst✝² : PseudoMetricSpace α
inst✝¹ : PseudoMetricSpace β
s t✝ u : Set α
x✝ y : α
Φ : α → β
inst✝ : ProperSpace α
h : IsClosed s
x z : α
hz : z ∈ s
t : Set α := s ∩ closedBall x (dist z x)
htc : IsCompact t
htne : Set.Nonempty t
⊢ ∃ y, y ∈ s ∧ infDist x t = dist x y
[PROOFSTEP]
obtain ⟨y, ⟨hys, -⟩, hyd⟩ : ∃ y ∈ t, infDist x t = dist x y := htc.exists_infDist_eq_dist htne x
[GOAL]
case intro.intro.intro.intro
ι : Sort u_1
α : Type u
β : Type v
inst✝² : PseudoMetricSpace α
inst✝¹ : PseudoMetricSpace β
s t✝ u : Set α
x✝ y✝ : α
Φ : α → β
inst✝ : ProperSpace α
h : IsClosed s
x z : α
hz : z ∈ s
t : Set α := s ∩ closedBall x (dist z x)
htc : IsCompact t
htne : Set.Nonempty t
y : α
hyd : infDist x t = dist x y
hys : y ∈ s
⊢ ∃ y, y ∈ s ∧ infDist x t = dist x y
[PROOFSTEP]
exact ⟨y, hys, hyd⟩
[GOAL]
ι : Sort u_1
α : Type u
β : Type v
inst✝² : PseudoMetricSpace α
inst✝¹ : PseudoMetricSpace β
s t u : Set α
x✝ y : α
Φ : α → β
inst✝ : ProperSpace α
hne : Set.Nonempty s
x : α
⊢ ∃ y, y ∈ closure s ∧ infDist x s = dist x y
[PROOFSTEP]
simpa only [infDist_closure] using isClosed_closure.exists_infDist_eq_dist hne.closure x
[GOAL]
ι : Sort u_1
α : Type u
β : Type v
inst✝¹ : PseudoMetricSpace α
inst✝ : PseudoMetricSpace β
s t u : Set α
x y : α
Φ : α → β
⊢ 0 ≤ hausdorffDist s t
[PROOFSTEP]
simp [hausdorffDist]
[GOAL]
ι : Sort u_1
α : Type u
β : Type v
inst✝¹ : PseudoMetricSpace α
inst✝ : PseudoMetricSpace β
s t u : Set α
x y : α
Φ : α → β
hs : Set.Nonempty s
ht : Set.Nonempty t
bs : Bounded s
bt : Bounded t
⊢ hausdorffEdist s t ≠ ⊤
[PROOFSTEP]
rcases hs with ⟨cs, hcs⟩
[GOAL]
case intro
ι : Sort u_1
α : Type u
β : Type v
inst✝¹ : PseudoMetricSpace α
inst✝ : PseudoMetricSpace β
s t u : Set α
x y : α
Φ : α → β
ht : Set.Nonempty t
bs : Bounded s
bt : Bounded t
cs : α
hcs : cs ∈ s
⊢ hausdorffEdist s t ≠ ⊤
[PROOFSTEP]
rcases ht with ⟨ct, hct⟩
[GOAL]
case intro.intro
ι : Sort u_1
α : Type u
β : Type v
inst✝¹ : PseudoMetricSpace α
inst✝ : PseudoMetricSpace β
s t u : Set α
x y : α
Φ : α → β
bs : Bounded s
bt : Bounded t
cs : α
hcs : cs ∈ s
ct : α
hct : ct ∈ t
⊢ hausdorffEdist s t ≠ ⊤
[PROOFSTEP]
rcases(bounded_iff_subset_ball ct).1 bs with ⟨rs, hrs⟩
[GOAL]
case intro.intro.intro
ι : Sort u_1
α : Type u
β : Type v
inst✝¹ : PseudoMetricSpace α
inst✝ : PseudoMetricSpace β
s t u : Set α
x y : α
Φ : α → β
bs : Bounded s
bt : Bounded t
cs : α
hcs : cs ∈ s
ct : α
hct : ct ∈ t
rs : ℝ
hrs : s ⊆ closedBall ct rs
⊢ hausdorffEdist s t ≠ ⊤
[PROOFSTEP]
rcases(bounded_iff_subset_ball cs).1 bt with ⟨rt, hrt⟩
[GOAL]
case intro.intro.intro.intro
ι : Sort u_1
α : Type u
β : Type v
inst✝¹ : PseudoMetricSpace α
inst✝ : PseudoMetricSpace β
s t u : Set α
x y : α
Φ : α → β
bs : Bounded s
bt : Bounded t
cs : α
hcs : cs ∈ s
ct : α
hct : ct ∈ t
rs : ℝ
hrs : s ⊆ closedBall ct rs
rt : ℝ
hrt : t ⊆ closedBall cs rt
⊢ hausdorffEdist s t ≠ ⊤
[PROOFSTEP]
have : hausdorffEdist s t ≤ ENNReal.ofReal (max rs rt) :=
  by
  apply hausdorffEdist_le_of_mem_edist
  · intro x xs
    exists ct, hct
    have : dist x ct ≤ max rs rt := le_trans (hrs xs) (le_max_left _ _)
    rwa [edist_dist, ENNReal.ofReal_le_ofReal_iff]
    exact le_trans dist_nonneg this
  · intro x xt
    exists cs, hcs
    have : dist x cs ≤ max rs rt := le_trans (hrt xt) (le_max_right _ _)
    rwa [edist_dist, ENNReal.ofReal_le_ofReal_iff]
    exact le_trans dist_nonneg this
[GOAL]
ι : Sort u_1
α : Type u
β : Type v
inst✝¹ : PseudoMetricSpace α
inst✝ : PseudoMetricSpace β
s t u : Set α
x y : α
Φ : α → β
bs : Bounded s
bt : Bounded t
cs : α
hcs : cs ∈ s
ct : α
hct : ct ∈ t
rs : ℝ
hrs : s ⊆ closedBall ct rs
rt : ℝ
hrt : t ⊆ closedBall cs rt
⊢ hausdorffEdist s t ≤ ENNReal.ofReal (max rs rt)
[PROOFSTEP]
apply hausdorffEdist_le_of_mem_edist
[GOAL]
case H1
ι : Sort u_1
α : Type u
β : Type v
inst✝¹ : PseudoMetricSpace α
inst✝ : PseudoMetricSpace β
s t u : Set α
x y : α
Φ : α → β
bs : Bounded s
bt : Bounded t
cs : α
hcs : cs ∈ s
ct : α
hct : ct ∈ t
rs : ℝ
hrs : s ⊆ closedBall ct rs
rt : ℝ
hrt : t ⊆ closedBall cs rt
⊢ ∀ (x : α), x ∈ s → ∃ y, y ∈ t ∧ edist x y ≤ ENNReal.ofReal (max rs rt)
[PROOFSTEP]
intro x xs
[GOAL]
case H1
ι : Sort u_1
α : Type u
β : Type v
inst✝¹ : PseudoMetricSpace α
inst✝ : PseudoMetricSpace β
s t u : Set α
x✝ y : α
Φ : α → β
bs : Bounded s
bt : Bounded t
cs : α
hcs : cs ∈ s
ct : α
hct : ct ∈ t
rs : ℝ
hrs : s ⊆ closedBall ct rs
rt : ℝ
hrt : t ⊆ closedBall cs rt
x : α
xs : x ∈ s
⊢ ∃ y, y ∈ t ∧ edist x y ≤ ENNReal.ofReal (max rs rt)
[PROOFSTEP]
exists ct, hct
[GOAL]
case H1
ι : Sort u_1
α : Type u
β : Type v
inst✝¹ : PseudoMetricSpace α
inst✝ : PseudoMetricSpace β
s t u : Set α
x✝ y : α
Φ : α → β
bs : Bounded s
bt : Bounded t
cs : α
hcs : cs ∈ s
ct : α
hct : ct ∈ t
rs : ℝ
hrs : s ⊆ closedBall ct rs
rt : ℝ
hrt : t ⊆ closedBall cs rt
x : α
xs : x ∈ s
⊢ edist x ct ≤ ENNReal.ofReal (max rs rt)
[PROOFSTEP]
have : dist x ct ≤ max rs rt := le_trans (hrs xs) (le_max_left _ _)
[GOAL]
case H1
ι : Sort u_1
α : Type u
β : Type v
inst✝¹ : PseudoMetricSpace α
inst✝ : PseudoMetricSpace β
s t u : Set α
x✝ y : α
Φ : α → β
bs : Bounded s
bt : Bounded t
cs : α
hcs : cs ∈ s
ct : α
hct : ct ∈ t
rs : ℝ
hrs : s ⊆ closedBall ct rs
rt : ℝ
hrt : t ⊆ closedBall cs rt
x : α
xs : x ∈ s
this : dist x ct ≤ max rs rt
⊢ edist x ct ≤ ENNReal.ofReal (max rs rt)
[PROOFSTEP]
rwa [edist_dist, ENNReal.ofReal_le_ofReal_iff]
[GOAL]
case H1
ι : Sort u_1
α : Type u
β : Type v
inst✝¹ : PseudoMetricSpace α
inst✝ : PseudoMetricSpace β
s t u : Set α
x✝ y : α
Φ : α → β
bs : Bounded s
bt : Bounded t
cs : α
hcs : cs ∈ s
ct : α
hct : ct ∈ t
rs : ℝ
hrs : s ⊆ closedBall ct rs
rt : ℝ
hrt : t ⊆ closedBall cs rt
x : α
xs : x ∈ s
this : dist x ct ≤ max rs rt
⊢ 0 ≤ max rs rt
[PROOFSTEP]
exact le_trans dist_nonneg this
[GOAL]
case H2
ι : Sort u_1
α : Type u
β : Type v
inst✝¹ : PseudoMetricSpace α
inst✝ : PseudoMetricSpace β
s t u : Set α
x y : α
Φ : α → β
bs : Bounded s
bt : Bounded t
cs : α
hcs : cs ∈ s
ct : α
hct : ct ∈ t
rs : ℝ
hrs : s ⊆ closedBall ct rs
rt : ℝ
hrt : t ⊆ closedBall cs rt
⊢ ∀ (x : α), x ∈ t → ∃ y, y ∈ s ∧ edist x y ≤ ENNReal.ofReal (max rs rt)
[PROOFSTEP]
intro x xt
[GOAL]
case H2
ι : Sort u_1
α : Type u
β : Type v
inst✝¹ : PseudoMetricSpace α
inst✝ : PseudoMetricSpace β
s t u : Set α
x✝ y : α
Φ : α → β
bs : Bounded s
bt : Bounded t
cs : α
hcs : cs ∈ s
ct : α
hct : ct ∈ t
rs : ℝ
hrs : s ⊆ closedBall ct rs
rt : ℝ
hrt : t ⊆ closedBall cs rt
x : α
xt : x ∈ t
⊢ ∃ y, y ∈ s ∧ edist x y ≤ ENNReal.ofReal (max rs rt)
[PROOFSTEP]
exists cs, hcs
[GOAL]
case H2
ι : Sort u_1
α : Type u
β : Type v
inst✝¹ : PseudoMetricSpace α
inst✝ : PseudoMetricSpace β
s t u : Set α
x✝ y : α
Φ : α → β
bs : Bounded s
bt : Bounded t
cs : α
hcs : cs ∈ s
ct : α
hct : ct ∈ t
rs : ℝ
hrs : s ⊆ closedBall ct rs
rt : ℝ
hrt : t ⊆ closedBall cs rt
x : α
xt : x ∈ t
⊢ edist x cs ≤ ENNReal.ofReal (max rs rt)
[PROOFSTEP]
have : dist x cs ≤ max rs rt := le_trans (hrt xt) (le_max_right _ _)
[GOAL]
case H2
ι : Sort u_1
α : Type u
β : Type v
inst✝¹ : PseudoMetricSpace α
inst✝ : PseudoMetricSpace β
s t u : Set α
x✝ y : α
Φ : α → β
bs : Bounded s
bt : Bounded t
cs : α
hcs : cs ∈ s
ct : α
hct : ct ∈ t
rs : ℝ
hrs : s ⊆ closedBall ct rs
rt : ℝ
hrt : t ⊆ closedBall cs rt
x : α
xt : x ∈ t
this : dist x cs ≤ max rs rt
⊢ edist x cs ≤ ENNReal.ofReal (max rs rt)
[PROOFSTEP]
rwa [edist_dist, ENNReal.ofReal_le_ofReal_iff]
[GOAL]
case H2
ι : Sort u_1
α : Type u
β : Type v
inst✝¹ : PseudoMetricSpace α
inst✝ : PseudoMetricSpace β
s t u : Set α
x✝ y : α
Φ : α → β
bs : Bounded s
bt : Bounded t
cs : α
hcs : cs ∈ s
ct : α
hct : ct ∈ t
rs : ℝ
hrs : s ⊆ closedBall ct rs
rt : ℝ
hrt : t ⊆ closedBall cs rt
x : α
xt : x ∈ t
this : dist x cs ≤ max rs rt
⊢ 0 ≤ max rs rt
[PROOFSTEP]
exact le_trans dist_nonneg this
[GOAL]
case intro.intro.intro.intro
ι : Sort u_1
α : Type u
β : Type v
inst✝¹ : PseudoMetricSpace α
inst✝ : PseudoMetricSpace β
s t u : Set α
x y : α
Φ : α → β
bs : Bounded s
bt : Bounded t
cs : α
hcs : cs ∈ s
ct : α
hct : ct ∈ t
rs : ℝ
hrs : s ⊆ closedBall ct rs
rt : ℝ
hrt : t ⊆ closedBall cs rt
this : hausdorffEdist s t ≤ ENNReal.ofReal (max rs rt)
⊢ hausdorffEdist s t ≠ ⊤
[PROOFSTEP]
exact ne_top_of_le_ne_top ENNReal.ofReal_ne_top this
[GOAL]
ι : Sort u_1
α : Type u
β : Type v
inst✝¹ : PseudoMetricSpace α
inst✝ : PseudoMetricSpace β
s t u : Set α
x y : α
Φ : α → β
⊢ hausdorffDist s s = 0
[PROOFSTEP]
simp [hausdorffDist]
[GOAL]
ι : Sort u_1
α : Type u
β : Type v
inst✝¹ : PseudoMetricSpace α
inst✝ : PseudoMetricSpace β
s t u : Set α
x y : α
Φ : α → β
⊢ hausdorffDist s t = hausdorffDist t s
[PROOFSTEP]
simp [hausdorffDist, hausdorffEdist_comm]
[GOAL]
ι : Sort u_1
α : Type u
β : Type v
inst✝¹ : PseudoMetricSpace α
inst✝ : PseudoMetricSpace β
s t u : Set α
x y : α
Φ : α → β
⊢ hausdorffDist s ∅ = 0
[PROOFSTEP]
cases' s.eq_empty_or_nonempty with h h
[GOAL]
case inl
ι : Sort u_1
α : Type u
β : Type v
inst✝¹ : PseudoMetricSpace α
inst✝ : PseudoMetricSpace β
s t u : Set α
x y : α
Φ : α → β
h : s = ∅
⊢ hausdorffDist s ∅ = 0
[PROOFSTEP]
simp [h]
[GOAL]
case inr
ι : Sort u_1
α : Type u
β : Type v
inst✝¹ : PseudoMetricSpace α
inst✝ : PseudoMetricSpace β
s t u : Set α
x y : α
Φ : α → β
h : Set.Nonempty s
⊢ hausdorffDist s ∅ = 0
[PROOFSTEP]
simp [hausdorffDist, hausdorffEdist_empty h]
[GOAL]
ι : Sort u_1
α : Type u
β : Type v
inst✝¹ : PseudoMetricSpace α
inst✝ : PseudoMetricSpace β
s t u : Set α
x y : α
Φ : α → β
⊢ hausdorffDist ∅ s = 0
[PROOFSTEP]
simp [hausdorffDist_comm]
[GOAL]
ι : Sort u_1
α : Type u
β : Type v
inst✝¹ : PseudoMetricSpace α
inst✝ : PseudoMetricSpace β
s t u : Set α
x y : α
Φ : α → β
r : ℝ
hr : 0 ≤ r
H1 : ∀ (x : α), x ∈ s → infDist x t ≤ r
H2 : ∀ (x : α), x ∈ t → infDist x s ≤ r
⊢ hausdorffDist s t ≤ r
[PROOFSTEP]
by_cases h1 : hausdorffEdist s t = ⊤
[GOAL]
case pos
ι : Sort u_1
α : Type u
β : Type v
inst✝¹ : PseudoMetricSpace α
inst✝ : PseudoMetricSpace β
s t u : Set α
x y : α
Φ : α → β
r : ℝ
hr : 0 ≤ r
H1 : ∀ (x : α), x ∈ s → infDist x t ≤ r
H2 : ∀ (x : α), x ∈ t → infDist x s ≤ r
h1 : hausdorffEdist s t = ⊤
⊢ hausdorffDist s t ≤ r
[PROOFSTEP]
rwa [hausdorffDist, h1, ENNReal.top_toReal]
[GOAL]
case neg
ι : Sort u_1
α : Type u
β : Type v
inst✝¹ : PseudoMetricSpace α
inst✝ : PseudoMetricSpace β
s t u : Set α
x y : α
Φ : α → β
r : ℝ
hr : 0 ≤ r
H1 : ∀ (x : α), x ∈ s → infDist x t ≤ r
H2 : ∀ (x : α), x ∈ t → infDist x s ≤ r
h1 : ¬hausdorffEdist s t = ⊤
⊢ hausdorffDist s t ≤ r
[PROOFSTEP]
cases' s.eq_empty_or_nonempty with hs hs
[GOAL]
case neg.inl
ι : Sort u_1
α : Type u
β : Type v
inst✝¹ : PseudoMetricSpace α
inst✝ : PseudoMetricSpace β
s t u : Set α
x y : α
Φ : α → β
r : ℝ
hr : 0 ≤ r
H1 : ∀ (x : α), x ∈ s → infDist x t ≤ r
H2 : ∀ (x : α), x ∈ t → infDist x s ≤ r
h1 : ¬hausdorffEdist s t = ⊤
hs : s = ∅
⊢ hausdorffDist s t ≤ r
[PROOFSTEP]
rwa [hs, hausdorffDist_empty']
[GOAL]
case neg.inr
ι : Sort u_1
α : Type u
β : Type v
inst✝¹ : PseudoMetricSpace α
inst✝ : PseudoMetricSpace β
s t u : Set α
x y : α
Φ : α → β
r : ℝ
hr : 0 ≤ r
H1 : ∀ (x : α), x ∈ s → infDist x t ≤ r
H2 : ∀ (x : α), x ∈ t → infDist x s ≤ r
h1 : ¬hausdorffEdist s t = ⊤
hs : Set.Nonempty s
⊢ hausdorffDist s t ≤ r
[PROOFSTEP]
cases' t.eq_empty_or_nonempty with ht ht
[GOAL]
case neg.inr.inl
ι : Sort u_1
α : Type u
β : Type v
inst✝¹ : PseudoMetricSpace α
inst✝ : PseudoMetricSpace β
s t u : Set α
x y : α
Φ : α → β
r : ℝ
hr : 0 ≤ r
H1 : ∀ (x : α), x ∈ s → infDist x t ≤ r
H2 : ∀ (x : α), x ∈ t → infDist x s ≤ r
h1 : ¬hausdorffEdist s t = ⊤
hs : Set.Nonempty s
ht : t = ∅
⊢ hausdorffDist s t ≤ r
[PROOFSTEP]
rwa [ht, hausdorffDist_empty]
[GOAL]
case neg.inr.inr
ι : Sort u_1
α : Type u
β : Type v
inst✝¹ : PseudoMetricSpace α
inst✝ : PseudoMetricSpace β
s t u : Set α
x y : α
Φ : α → β
r : ℝ
hr : 0 ≤ r
H1 : ∀ (x : α), x ∈ s → infDist x t ≤ r
H2 : ∀ (x : α), x ∈ t → infDist x s ≤ r
h1 : ¬hausdorffEdist s t = ⊤
hs : Set.Nonempty s
ht : Set.Nonempty t
⊢ hausdorffDist s t ≤ r
[PROOFSTEP]
have : hausdorffEdist s t ≤ ENNReal.ofReal r :=
  by
  apply hausdorffEdist_le_of_infEdist _ _
  · intro x hx
    have I := H1 x hx
    rwa [infDist, ← ENNReal.toReal_ofReal hr, ENNReal.toReal_le_toReal (infEdist_ne_top ht) ENNReal.ofReal_ne_top] at I 
  · intro x hx
    have I := H2 x hx
    rwa [infDist, ← ENNReal.toReal_ofReal hr, ENNReal.toReal_le_toReal (infEdist_ne_top hs) ENNReal.ofReal_ne_top] at I 
[GOAL]
ι : Sort u_1
α : Type u
β : Type v
inst✝¹ : PseudoMetricSpace α
inst✝ : PseudoMetricSpace β
s t u : Set α
x y : α
Φ : α → β
r : ℝ
hr : 0 ≤ r
H1 : ∀ (x : α), x ∈ s → infDist x t ≤ r
H2 : ∀ (x : α), x ∈ t → infDist x s ≤ r
h1 : ¬hausdorffEdist s t = ⊤
hs : Set.Nonempty s
ht : Set.Nonempty t
⊢ hausdorffEdist s t ≤ ENNReal.ofReal r
[PROOFSTEP]
apply hausdorffEdist_le_of_infEdist _ _
[GOAL]
ι : Sort u_1
α : Type u
β : Type v
inst✝¹ : PseudoMetricSpace α
inst✝ : PseudoMetricSpace β
s t u : Set α
x y : α
Φ : α → β
r : ℝ
hr : 0 ≤ r
H1 : ∀ (x : α), x ∈ s → infDist x t ≤ r
H2 : ∀ (x : α), x ∈ t → infDist x s ≤ r
h1 : ¬hausdorffEdist s t = ⊤
hs : Set.Nonempty s
ht : Set.Nonempty t
⊢ ∀ (x : α), x ∈ s → infEdist x t ≤ ENNReal.ofReal r
[PROOFSTEP]
intro x hx
[GOAL]
ι : Sort u_1
α : Type u
β : Type v
inst✝¹ : PseudoMetricSpace α
inst✝ : PseudoMetricSpace β
s t u : Set α
x✝ y : α
Φ : α → β
r : ℝ
hr : 0 ≤ r
H1 : ∀ (x : α), x ∈ s → infDist x t ≤ r
H2 : ∀ (x : α), x ∈ t → infDist x s ≤ r
h1 : ¬hausdorffEdist s t = ⊤
hs : Set.Nonempty s
ht : Set.Nonempty t
x : α
hx : x ∈ s
⊢ infEdist x t ≤ ENNReal.ofReal r
[PROOFSTEP]
have I := H1 x hx
[GOAL]
ι : Sort u_1
α : Type u
β : Type v
inst✝¹ : PseudoMetricSpace α
inst✝ : PseudoMetricSpace β
s t u : Set α
x✝ y : α
Φ : α → β
r : ℝ
hr : 0 ≤ r
H1 : ∀ (x : α), x ∈ s → infDist x t ≤ r
H2 : ∀ (x : α), x ∈ t → infDist x s ≤ r
h1 : ¬hausdorffEdist s t = ⊤
hs : Set.Nonempty s
ht : Set.Nonempty t
x : α
hx : x ∈ s
I : infDist x t ≤ r
⊢ infEdist x t ≤ ENNReal.ofReal r
[PROOFSTEP]
rwa [infDist, ← ENNReal.toReal_ofReal hr, ENNReal.toReal_le_toReal (infEdist_ne_top ht) ENNReal.ofReal_ne_top] at I 
[GOAL]
ι : Sort u_1
α : Type u
β : Type v
inst✝¹ : PseudoMetricSpace α
inst✝ : PseudoMetricSpace β
s t u : Set α
x y : α
Φ : α → β
r : ℝ
hr : 0 ≤ r
H1 : ∀ (x : α), x ∈ s → infDist x t ≤ r
H2 : ∀ (x : α), x ∈ t → infDist x s ≤ r
h1 : ¬hausdorffEdist s t = ⊤
hs : Set.Nonempty s
ht : Set.Nonempty t
⊢ ∀ (x : α), x ∈ t → infEdist x s ≤ ENNReal.ofReal r
[PROOFSTEP]
intro x hx
[GOAL]
ι : Sort u_1
α : Type u
β : Type v
inst✝¹ : PseudoMetricSpace α
inst✝ : PseudoMetricSpace β
s t u : Set α
x✝ y : α
Φ : α → β
r : ℝ
hr : 0 ≤ r
H1 : ∀ (x : α), x ∈ s → infDist x t ≤ r
H2 : ∀ (x : α), x ∈ t → infDist x s ≤ r
h1 : ¬hausdorffEdist s t = ⊤
hs : Set.Nonempty s
ht : Set.Nonempty t
x : α
hx : x ∈ t
⊢ infEdist x s ≤ ENNReal.ofReal r
[PROOFSTEP]
have I := H2 x hx
[GOAL]
ι : Sort u_1
α : Type u
β : Type v
inst✝¹ : PseudoMetricSpace α
inst✝ : PseudoMetricSpace β
s t u : Set α
x✝ y : α
Φ : α → β
r : ℝ
hr : 0 ≤ r
H1 : ∀ (x : α), x ∈ s → infDist x t ≤ r
H2 : ∀ (x : α), x ∈ t → infDist x s ≤ r
h1 : ¬hausdorffEdist s t = ⊤
hs : Set.Nonempty s
ht : Set.Nonempty t
x : α
hx : x ∈ t
I : infDist x s ≤ r
⊢ infEdist x s ≤ ENNReal.ofReal r
[PROOFSTEP]
rwa [infDist, ← ENNReal.toReal_ofReal hr, ENNReal.toReal_le_toReal (infEdist_ne_top hs) ENNReal.ofReal_ne_top] at I 
[GOAL]
case neg.inr.inr
ι : Sort u_1
α : Type u
β : Type v
inst✝¹ : PseudoMetricSpace α
inst✝ : PseudoMetricSpace β
s t u : Set α
x y : α
Φ : α → β
r : ℝ
hr : 0 ≤ r
H1 : ∀ (x : α), x ∈ s → infDist x t ≤ r
H2 : ∀ (x : α), x ∈ t → infDist x s ≤ r
h1 : ¬hausdorffEdist s t = ⊤
hs : Set.Nonempty s
ht : Set.Nonempty t
this : hausdorffEdist s t ≤ ENNReal.ofReal r
⊢ hausdorffDist s t ≤ r
[PROOFSTEP]
rwa [hausdorffDist, ← ENNReal.toReal_ofReal hr, ENNReal.toReal_le_toReal h1 ENNReal.ofReal_ne_top]
[GOAL]
ι : Sort u_1
α : Type u
β : Type v
inst✝¹ : PseudoMetricSpace α
inst✝ : PseudoMetricSpace β
s t u : Set α
x y : α
Φ : α → β
r : ℝ
hr : 0 ≤ r
H1 : ∀ (x : α), x ∈ s → ∃ y, y ∈ t ∧ dist x y ≤ r
H2 : ∀ (x : α), x ∈ t → ∃ y, y ∈ s ∧ dist x y ≤ r
⊢ hausdorffDist s t ≤ r
[PROOFSTEP]
apply hausdorffDist_le_of_infDist hr
[GOAL]
case H1
ι : Sort u_1
α : Type u
β : Type v
inst✝¹ : PseudoMetricSpace α
inst✝ : PseudoMetricSpace β
s t u : Set α
x y : α
Φ : α → β
r : ℝ
hr : 0 ≤ r
H1 : ∀ (x : α), x ∈ s → ∃ y, y ∈ t ∧ dist x y ≤ r
H2 : ∀ (x : α), x ∈ t → ∃ y, y ∈ s ∧ dist x y ≤ r
⊢ ∀ (x : α), x ∈ s → infDist x t ≤ r
[PROOFSTEP]
intro x xs
[GOAL]
case H1
ι : Sort u_1
α : Type u
β : Type v
inst✝¹ : PseudoMetricSpace α
inst✝ : PseudoMetricSpace β
s t u : Set α
x✝ y : α
Φ : α → β
r : ℝ
hr : 0 ≤ r
H1 : ∀ (x : α), x ∈ s → ∃ y, y ∈ t ∧ dist x y ≤ r
H2 : ∀ (x : α), x ∈ t → ∃ y, y ∈ s ∧ dist x y ≤ r
x : α
xs : x ∈ s
⊢ infDist x t ≤ r
[PROOFSTEP]
rcases H1 x xs with ⟨y, yt, hy⟩
[GOAL]
case H1.intro.intro
ι : Sort u_1
α : Type u
β : Type v
inst✝¹ : PseudoMetricSpace α
inst✝ : PseudoMetricSpace β
s t u : Set α
x✝ y✝ : α
Φ : α → β
r : ℝ
hr : 0 ≤ r
H1 : ∀ (x : α), x ∈ s → ∃ y, y ∈ t ∧ dist x y ≤ r
H2 : ∀ (x : α), x ∈ t → ∃ y, y ∈ s ∧ dist x y ≤ r
x : α
xs : x ∈ s
y : α
yt : y ∈ t
hy : dist x y ≤ r
⊢ infDist x t ≤ r
[PROOFSTEP]
exact le_trans (infDist_le_dist_of_mem yt) hy
[GOAL]
case H2
ι : Sort u_1
α : Type u
β : Type v
inst✝¹ : PseudoMetricSpace α
inst✝ : PseudoMetricSpace β
s t u : Set α
x y : α
Φ : α → β
r : ℝ
hr : 0 ≤ r
H1 : ∀ (x : α), x ∈ s → ∃ y, y ∈ t ∧ dist x y ≤ r
H2 : ∀ (x : α), x ∈ t → ∃ y, y ∈ s ∧ dist x y ≤ r
⊢ ∀ (x : α), x ∈ t → infDist x s ≤ r
[PROOFSTEP]
intro x xt
[GOAL]
case H2
ι : Sort u_1
α : Type u
β : Type v
inst✝¹ : PseudoMetricSpace α
inst✝ : PseudoMetricSpace β
s t u : Set α
x✝ y : α
Φ : α → β
r : ℝ
hr : 0 ≤ r
H1 : ∀ (x : α), x ∈ s → ∃ y, y ∈ t ∧ dist x y ≤ r
H2 : ∀ (x : α), x ∈ t → ∃ y, y ∈ s ∧ dist x y ≤ r
x : α
xt : x ∈ t
⊢ infDist x s ≤ r
[PROOFSTEP]
rcases H2 x xt with ⟨y, ys, hy⟩
[GOAL]
case H2.intro.intro
ι : Sort u_1
α : Type u
β : Type v
inst✝¹ : PseudoMetricSpace α
inst✝ : PseudoMetricSpace β
s t u : Set α
x✝ y✝ : α
Φ : α → β
r : ℝ
hr : 0 ≤ r
H1 : ∀ (x : α), x ∈ s → ∃ y, y ∈ t ∧ dist x y ≤ r
H2 : ∀ (x : α), x ∈ t → ∃ y, y ∈ s ∧ dist x y ≤ r
x : α
xt : x ∈ t
y : α
ys : y ∈ s
hy : dist x y ≤ r
⊢ infDist x s ≤ r
[PROOFSTEP]
exact le_trans (infDist_le_dist_of_mem ys) hy
[GOAL]
ι : Sort u_1
α : Type u
β : Type v
inst✝¹ : PseudoMetricSpace α
inst✝ : PseudoMetricSpace β
s t u : Set α
x y : α
Φ : α → β
hs : Set.Nonempty s
bs : Bounded s
ht : Set.Nonempty t
bt : Bounded t
⊢ hausdorffDist s t ≤ diam (s ∪ t)
[PROOFSTEP]
rcases hs with ⟨x, xs⟩
[GOAL]
case intro
ι : Sort u_1
α : Type u
β : Type v
inst✝¹ : PseudoMetricSpace α
inst✝ : PseudoMetricSpace β
s t u : Set α
x✝ y : α
Φ : α → β
bs : Bounded s
ht : Set.Nonempty t
bt : Bounded t
x : α
xs : x ∈ s
⊢ hausdorffDist s t ≤ diam (s ∪ t)
[PROOFSTEP]
rcases ht with ⟨y, yt⟩
[GOAL]
case intro.intro
ι : Sort u_1
α : Type u
β : Type v
inst✝¹ : PseudoMetricSpace α
inst✝ : PseudoMetricSpace β
s t u : Set α
x✝ y✝ : α
Φ : α → β
bs : Bounded s
bt : Bounded t
x : α
xs : x ∈ s
y : α
yt : y ∈ t
⊢ hausdorffDist s t ≤ diam (s ∪ t)
[PROOFSTEP]
refine hausdorffDist_le_of_mem_dist diam_nonneg ?_ ?_
[GOAL]
case intro.intro.refine_1
ι : Sort u_1
α : Type u
β : Type v
inst✝¹ : PseudoMetricSpace α
inst✝ : PseudoMetricSpace β
s t u : Set α
x✝ y✝ : α
Φ : α → β
bs : Bounded s
bt : Bounded t
x : α
xs : x ∈ s
y : α
yt : y ∈ t
⊢ ∀ (x : α), x ∈ s → ∃ y, y ∈ t ∧ dist x y ≤ diam (s ∪ t)
[PROOFSTEP]
exact fun z hz =>
  ⟨y, yt, dist_le_diam_of_mem (bounded_union.2 ⟨bs, bt⟩) (subset_union_left _ _ hz) (subset_union_right _ _ yt)⟩
[GOAL]
case intro.intro.refine_2
ι : Sort u_1
α : Type u
β : Type v
inst✝¹ : PseudoMetricSpace α
inst✝ : PseudoMetricSpace β
s t u : Set α
x✝ y✝ : α
Φ : α → β
bs : Bounded s
bt : Bounded t
x : α
xs : x ∈ s
y : α
yt : y ∈ t
⊢ ∀ (x : α), x ∈ t → ∃ y, y ∈ s ∧ dist x y ≤ diam (s ∪ t)
[PROOFSTEP]
exact fun z hz =>
  ⟨x, xs, dist_le_diam_of_mem (bounded_union.2 ⟨bs, bt⟩) (subset_union_right _ _ hz) (subset_union_left _ _ xs)⟩
[GOAL]
ι : Sort u_1
α : Type u
β : Type v
inst✝¹ : PseudoMetricSpace α
inst✝ : PseudoMetricSpace β
s t u : Set α
x y : α
Φ : α → β
r : ℝ
h : x ∈ s
H : hausdorffDist s t < r
fin : hausdorffEdist s t ≠ ⊤
⊢ ∃ y, y ∈ t ∧ dist x y < r
[PROOFSTEP]
have r0 : 0 < r := lt_of_le_of_lt hausdorffDist_nonneg H
[GOAL]
ι : Sort u_1
α : Type u
β : Type v
inst✝¹ : PseudoMetricSpace α
inst✝ : PseudoMetricSpace β
s t u : Set α
x y : α
Φ : α → β
r : ℝ
h : x ∈ s
H : hausdorffDist s t < r
fin : hausdorffEdist s t ≠ ⊤
r0 : 0 < r
⊢ ∃ y, y ∈ t ∧ dist x y < r
[PROOFSTEP]
have : hausdorffEdist s t < ENNReal.ofReal r := by
  rwa [hausdorffDist, ← ENNReal.toReal_ofReal (le_of_lt r0), ENNReal.toReal_lt_toReal fin ENNReal.ofReal_ne_top] at H 
[GOAL]
ι : Sort u_1
α : Type u
β : Type v
inst✝¹ : PseudoMetricSpace α
inst✝ : PseudoMetricSpace β
s t u : Set α
x y : α
Φ : α → β
r : ℝ
h : x ∈ s
H : hausdorffDist s t < r
fin : hausdorffEdist s t ≠ ⊤
r0 : 0 < r
⊢ hausdorffEdist s t < ENNReal.ofReal r
[PROOFSTEP]
rwa [hausdorffDist, ← ENNReal.toReal_ofReal (le_of_lt r0), ENNReal.toReal_lt_toReal fin ENNReal.ofReal_ne_top] at H 
[GOAL]
ι : Sort u_1
α : Type u
β : Type v
inst✝¹ : PseudoMetricSpace α
inst✝ : PseudoMetricSpace β
s t u : Set α
x y : α
Φ : α → β
r : ℝ
h : x ∈ s
H : hausdorffDist s t < r
fin : hausdorffEdist s t ≠ ⊤
r0 : 0 < r
this : hausdorffEdist s t < ENNReal.ofReal r
⊢ ∃ y, y ∈ t ∧ dist x y < r
[PROOFSTEP]
rcases exists_edist_lt_of_hausdorffEdist_lt h this with ⟨y, hy, yr⟩
[GOAL]
case intro.intro
ι : Sort u_1
α : Type u
β : Type v
inst✝¹ : PseudoMetricSpace α
inst✝ : PseudoMetricSpace β
s t u : Set α
x y✝ : α
Φ : α → β
r : ℝ
h : x ∈ s
H : hausdorffDist s t < r
fin : hausdorffEdist s t ≠ ⊤
r0 : 0 < r
this : hausdorffEdist s t < ENNReal.ofReal r
y : α
hy : y ∈ t
yr : edist x y < ENNReal.ofReal r
⊢ ∃ y, y ∈ t ∧ dist x y < r
[PROOFSTEP]
rw [edist_dist, ENNReal.ofReal_lt_ofReal_iff r0] at yr 
[GOAL]
case intro.intro
ι : Sort u_1
α : Type u
β : Type v
inst✝¹ : PseudoMetricSpace α
inst✝ : PseudoMetricSpace β
s t u : Set α
x y✝ : α
Φ : α → β
r : ℝ
h : x ∈ s
H : hausdorffDist s t < r
fin : hausdorffEdist s t ≠ ⊤
r0 : 0 < r
this : hausdorffEdist s t < ENNReal.ofReal r
y : α
hy : y ∈ t
yr : dist x y < r
⊢ ∃ y, y ∈ t ∧ dist x y < r
[PROOFSTEP]
exact ⟨y, hy, yr⟩
[GOAL]
ι : Sort u_1
α : Type u
β : Type v
inst✝¹ : PseudoMetricSpace α
inst✝ : PseudoMetricSpace β
s t u : Set α
x y : α
Φ : α → β
r : ℝ
h : y ∈ t
H : hausdorffDist s t < r
fin : hausdorffEdist s t ≠ ⊤
⊢ ∃ x, x ∈ s ∧ dist x y < r
[PROOFSTEP]
rw [hausdorffDist_comm] at H 
[GOAL]
ι : Sort u_1
α : Type u
β : Type v
inst✝¹ : PseudoMetricSpace α
inst✝ : PseudoMetricSpace β
s t u : Set α
x y : α
Φ : α → β
r : ℝ
h : y ∈ t
H : hausdorffDist t s < r
fin : hausdorffEdist s t ≠ ⊤
⊢ ∃ x, x ∈ s ∧ dist x y < r
[PROOFSTEP]
rw [hausdorffEdist_comm] at fin 
[GOAL]
ι : Sort u_1
α : Type u
β : Type v
inst✝¹ : PseudoMetricSpace α
inst✝ : PseudoMetricSpace β
s t u : Set α
x y : α
Φ : α → β
r : ℝ
h : y ∈ t
H : hausdorffDist t s < r
fin : hausdorffEdist t s ≠ ⊤
⊢ ∃ x, x ∈ s ∧ dist x y < r
[PROOFSTEP]
simpa [dist_comm] using exists_dist_lt_of_hausdorffDist_lt h H fin
[GOAL]
ι : Sort u_1
α : Type u
β : Type v
inst✝¹ : PseudoMetricSpace α
inst✝ : PseudoMetricSpace β
s t u : Set α
x y : α
Φ : α → β
fin : hausdorffEdist s t ≠ ⊤
⊢ infDist x t ≤ infDist x s + hausdorffDist s t
[PROOFSTEP]
refine toReal_le_add' infEdist_le_infEdist_add_hausdorffEdist (fun h ↦ ?_) (flip absurd fin)
[GOAL]
ι : Sort u_1
α : Type u
β : Type v
inst✝¹ : PseudoMetricSpace α
inst✝ : PseudoMetricSpace β
s t u : Set α
x y : α
Φ : α → β
fin : hausdorffEdist s t ≠ ⊤
h : infEdist x s = ⊤
⊢ infEdist x t = ⊤
[PROOFSTEP]
rw [infEdist_eq_top_iff, ← not_nonempty_iff_eq_empty] at h ⊢
[GOAL]
ι : Sort u_1
α : Type u
β : Type v
inst✝¹ : PseudoMetricSpace α
inst✝ : PseudoMetricSpace β
s t u : Set α
x y : α
Φ : α → β
fin : hausdorffEdist s t ≠ ⊤
h : ¬Set.Nonempty s
⊢ ¬Set.Nonempty t
[PROOFSTEP]
rw [hausdorffEdist_comm] at fin 
[GOAL]
ι : Sort u_1
α : Type u
β : Type v
inst✝¹ : PseudoMetricSpace α
inst✝ : PseudoMetricSpace β
s t u : Set α
x y : α
Φ : α → β
fin : hausdorffEdist t s ≠ ⊤
h : ¬Set.Nonempty s
⊢ ¬Set.Nonempty t
[PROOFSTEP]
exact mt (nonempty_of_hausdorffEdist_ne_top · fin) h
[GOAL]
ι : Sort u_1
α : Type u
β : Type v
inst✝¹ : PseudoMetricSpace α
inst✝ : PseudoMetricSpace β
s t u : Set α
x y : α
Φ : α → β
h : Isometry Φ
⊢ hausdorffDist (Φ '' s) (Φ '' t) = hausdorffDist s t
[PROOFSTEP]
simp [hausdorffDist, hausdorffEdist_image h]
[GOAL]
ι : Sort u_1
α : Type u
β : Type v
inst✝¹ : PseudoMetricSpace α
inst✝ : PseudoMetricSpace β
s t u : Set α
x y : α
Φ : α → β
fin : hausdorffEdist s t ≠ ⊤
⊢ hausdorffDist s u ≤ hausdorffDist s t + hausdorffDist t u
[PROOFSTEP]
refine toReal_le_add' hausdorffEdist_triangle (flip absurd fin) (not_imp_not.1 fun h ↦ ?_)
[GOAL]
ι : Sort u_1
α : Type u
β : Type v
inst✝¹ : PseudoMetricSpace α
inst✝ : PseudoMetricSpace β
s t u : Set α
x y : α
Φ : α → β
fin : hausdorffEdist s t ≠ ⊤
h : ¬hausdorffEdist s u = ⊤
⊢ ¬hausdorffEdist t u = ⊤
[PROOFSTEP]
rw [hausdorffEdist_comm] at fin 
[GOAL]
ι : Sort u_1
α : Type u
β : Type v
inst✝¹ : PseudoMetricSpace α
inst✝ : PseudoMetricSpace β
s t u : Set α
x y : α
Φ : α → β
fin : hausdorffEdist t s ≠ ⊤
h : ¬hausdorffEdist s u = ⊤
⊢ ¬hausdorffEdist t u = ⊤
[PROOFSTEP]
exact ne_top_of_le_ne_top (add_ne_top.2 ⟨fin, h⟩) hausdorffEdist_triangle
[GOAL]
ι : Sort u_1
α : Type u
β : Type v
inst✝¹ : PseudoMetricSpace α
inst✝ : PseudoMetricSpace β
s t u : Set α
x y : α
Φ : α → β
fin : hausdorffEdist t u ≠ ⊤
⊢ hausdorffDist s u ≤ hausdorffDist s t + hausdorffDist t u
[PROOFSTEP]
rw [hausdorffEdist_comm] at fin 
[GOAL]
ι : Sort u_1
α : Type u
β : Type v
inst✝¹ : PseudoMetricSpace α
inst✝ : PseudoMetricSpace β
s t u : Set α
x y : α
Φ : α → β
fin : hausdorffEdist u t ≠ ⊤
⊢ hausdorffDist s u ≤ hausdorffDist s t + hausdorffDist t u
[PROOFSTEP]
have I : hausdorffDist u s ≤ hausdorffDist u t + hausdorffDist t s := hausdorffDist_triangle fin
[GOAL]
ι : Sort u_1
α : Type u
β : Type v
inst✝¹ : PseudoMetricSpace α
inst✝ : PseudoMetricSpace β
s t u : Set α
x y : α
Φ : α → β
fin : hausdorffEdist u t ≠ ⊤
I : hausdorffDist u s ≤ hausdorffDist u t + hausdorffDist t s
⊢ hausdorffDist s u ≤ hausdorffDist s t + hausdorffDist t u
[PROOFSTEP]
simpa [add_comm, hausdorffDist_comm] using I
[GOAL]
ι : Sort u_1
α : Type u
β : Type v
inst✝¹ : PseudoMetricSpace α
inst✝ : PseudoMetricSpace β
s t u : Set α
x y : α
Φ : α → β
⊢ hausdorffDist s (closure s) = 0
[PROOFSTEP]
simp [hausdorffDist]
[GOAL]
ι : Sort u_1
α : Type u
β : Type v
inst✝¹ : PseudoMetricSpace α
inst✝ : PseudoMetricSpace β
s t u : Set α
x y : α
Φ : α → β
⊢ hausdorffDist (closure s) t = hausdorffDist s t
[PROOFSTEP]
simp [hausdorffDist]
[GOAL]
ι : Sort u_1
α : Type u
β : Type v
inst✝¹ : PseudoMetricSpace α
inst✝ : PseudoMetricSpace β
s t u : Set α
x y : α
Φ : α → β
⊢ hausdorffDist s (closure t) = hausdorffDist s t
[PROOFSTEP]
simp [hausdorffDist]
[GOAL]
ι : Sort u_1
α : Type u
β : Type v
inst✝¹ : PseudoMetricSpace α
inst✝ : PseudoMetricSpace β
s t u : Set α
x y : α
Φ : α → β
⊢ hausdorffDist (closure s) (closure t) = hausdorffDist s t
[PROOFSTEP]
simp [hausdorffDist]
[GOAL]
ι : Sort u_1
α : Type u
β : Type v
inst✝¹ : PseudoMetricSpace α
inst✝ : PseudoMetricSpace β
s t u : Set α
x y : α
Φ : α → β
fin : hausdorffEdist s t ≠ ⊤
⊢ hausdorffDist s t = 0 ↔ closure s = closure t
[PROOFSTEP]
simp [← hausdorffEdist_zero_iff_closure_eq_closure, hausdorffDist, ENNReal.toReal_eq_zero_iff, fin]
[GOAL]
ι : Sort u_1
α : Type u
β : Type v
inst✝¹ : PseudoMetricSpace α
inst✝ : PseudoMetricSpace β
s t u : Set α
x y : α
Φ : α → β
hs : IsClosed s
ht : IsClosed t
fin : hausdorffEdist s t ≠ ⊤
⊢ hausdorffDist s t = 0 ↔ s = t
[PROOFSTEP]
simp [← hausdorffEdist_zero_iff_eq_of_closed hs ht, hausdorffDist, ENNReal.toReal_eq_zero_iff, fin]
[GOAL]
ι : Sort u_1
α : Type u
β : Type v
inst✝ : PseudoEMetricSpace α
δ : ℝ
s : Set α
x✝ : α
E : Set α
x : α
h : ¬x ∈ closure E
⊢ ∀ᶠ (δ : ℝ) in 𝓝 0, ¬x ∈ thickening δ E
[PROOFSTEP]
obtain ⟨ε, ⟨ε_pos, ε_lt⟩⟩ := exists_real_pos_lt_infEdist_of_not_mem_closure h
[GOAL]
case intro.intro
ι : Sort u_1
α : Type u
β : Type v
inst✝ : PseudoEMetricSpace α
δ : ℝ
s : Set α
x✝ : α
E : Set α
x : α
h : ¬x ∈ closure E
ε : ℝ
ε_pos : 0 < ε
ε_lt : ENNReal.ofReal ε < infEdist x E
⊢ ∀ᶠ (δ : ℝ) in 𝓝 0, ¬x ∈ thickening δ E
[PROOFSTEP]
filter_upwards [eventually_lt_nhds ε_pos] with δ hδ
[GOAL]
case h
ι : Sort u_1
α : Type u
β : Type v
inst✝ : PseudoEMetricSpace α
δ✝ : ℝ
s : Set α
x✝ : α
E : Set α
x : α
h : ¬x ∈ closure E
ε : ℝ
ε_pos : 0 < ε
ε_lt : ENNReal.ofReal ε < infEdist x E
δ : ℝ
hδ : δ < ε
⊢ ¬x ∈ thickening δ E
[PROOFSTEP]
simp only [thickening, mem_setOf_eq, not_lt]
[GOAL]
case h
ι : Sort u_1
α : Type u
β : Type v
inst✝ : PseudoEMetricSpace α
δ✝ : ℝ
s : Set α
x✝ : α
E : Set α
x : α
h : ¬x ∈ closure E
ε : ℝ
ε_pos : 0 < ε
ε_lt : ENNReal.ofReal ε < infEdist x E
δ : ℝ
hδ : δ < ε
⊢ ENNReal.ofReal δ ≤ infEdist x E
[PROOFSTEP]
exact (ENNReal.ofReal_le_ofReal hδ.le).trans ε_lt.le
[GOAL]
ι : Sort u_1
α : Type u
β : Type v
inst✝ : PseudoEMetricSpace α
δ✝ : ℝ
s : Set α
x : α
δ : ℝ
⊢ thickening δ ∅ = ∅
[PROOFSTEP]
simp only [thickening, setOf_false, infEdist_empty, not_top_lt]
[GOAL]
ι : Sort u_1
α : Type u
β : Type v
inst✝ : PseudoEMetricSpace α
δ : ℝ
s : Set α
x : α
A : Set α
⊢ Pairwise (Disjoint on fun r => frontier (thickening r A))
[PROOFSTEP]
refine' (pairwise_disjoint_on _).2 fun r₁ r₂ hr => _
[GOAL]
ι : Sort u_1
α : Type u
β : Type v
inst✝ : PseudoEMetricSpace α
δ : ℝ
s : Set α
x : α
A : Set α
r₁ r₂ : ℝ
hr : r₁ < r₂
⊢ Disjoint (frontier (thickening r₁ A)) (frontier (thickening r₂ A))
[PROOFSTEP]
cases' le_total r₁ 0 with h₁ h₁
[GOAL]
case inl
ι : Sort u_1
α : Type u
β : Type v
inst✝ : PseudoEMetricSpace α
δ : ℝ
s : Set α
x : α
A : Set α
r₁ r₂ : ℝ
hr : r₁ < r₂
h₁ : r₁ ≤ 0
⊢ Disjoint (frontier (thickening r₁ A)) (frontier (thickening r₂ A))
[PROOFSTEP]
simp [thickening_of_nonpos h₁]
[GOAL]
case inr
ι : Sort u_1
α : Type u
β : Type v
inst✝ : PseudoEMetricSpace α
δ : ℝ
s : Set α
x : α
A : Set α
r₁ r₂ : ℝ
hr : r₁ < r₂
h₁ : 0 ≤ r₁
⊢ Disjoint (frontier (thickening r₁ A)) (frontier (thickening r₂ A))
[PROOFSTEP]
refine'
  ((disjoint_singleton.2 fun h => hr.ne _).preimage _).mono (frontier_thickening_subset _)
    (frontier_thickening_subset _)
[GOAL]
case inr
ι : Sort u_1
α : Type u
β : Type v
inst✝ : PseudoEMetricSpace α
δ : ℝ
s : Set α
x : α
A : Set α
r₁ r₂ : ℝ
hr : r₁ < r₂
h₁ : 0 ≤ r₁
h : ENNReal.ofReal r₁ = ENNReal.ofReal r₂
⊢ r₁ = r₂
[PROOFSTEP]
apply_fun ENNReal.toReal at h 
[GOAL]
case inr
ι : Sort u_1
α : Type u
β : Type v
inst✝ : PseudoEMetricSpace α
δ : ℝ
s : Set α
x : α
A : Set α
r₁ r₂ : ℝ
hr : r₁ < r₂
h₁ : 0 ≤ r₁
h : ENNReal.toReal (ENNReal.ofReal r₁) = ENNReal.toReal (ENNReal.ofReal r₂)
⊢ r₁ = r₂
[PROOFSTEP]
rwa [ENNReal.toReal_ofReal h₁, ENNReal.toReal_ofReal (h₁.trans hr.le)] at h 
[GOAL]
ι : Sort u_1
α : Type u
β : Type v
inst✝¹ : PseudoEMetricSpace α
δ : ℝ
s : Set α
x✝ : α
X : Type u
inst✝ : PseudoMetricSpace X
E : Set X
x : X
⊢ x ∈ thickening δ E ↔ ∃ z, z ∈ E ∧ dist x z < δ
[PROOFSTEP]
have key_iff : ∀ z : X, edist x z < ENNReal.ofReal δ ↔ dist x z < δ := fun z ↦ by
  rw [dist_edist, lt_ofReal_iff_toReal_lt (edist_ne_top _ _)]
[GOAL]
ι : Sort u_1
α : Type u
β : Type v
inst✝¹ : PseudoEMetricSpace α
δ : ℝ
s : Set α
x✝ : α
X : Type u
inst✝ : PseudoMetricSpace X
E : Set X
x z : X
⊢ edist x z < ENNReal.ofReal δ ↔ dist x z < δ
[PROOFSTEP]
rw [dist_edist, lt_ofReal_iff_toReal_lt (edist_ne_top _ _)]
[GOAL]
ι : Sort u_1
α : Type u
β : Type v
inst✝¹ : PseudoEMetricSpace α
δ : ℝ
s : Set α
x✝ : α
X : Type u
inst✝ : PseudoMetricSpace X
E : Set X
x : X
key_iff : ∀ (z : X), edist x z < ENNReal.ofReal δ ↔ dist x z < δ
⊢ x ∈ thickening δ E ↔ ∃ z, z ∈ E ∧ dist x z < δ
[PROOFSTEP]
simp_rw [mem_thickening_iff_exists_edist_lt, key_iff]
[GOAL]
ι : Sort u_1
α : Type u
β : Type v
inst✝¹ : PseudoEMetricSpace α
δ✝ : ℝ
s : Set α
x✝ : α
X : Type u
inst✝ : PseudoMetricSpace X
δ : ℝ
x : X
⊢ thickening δ {x} = ball x δ
[PROOFSTEP]
ext
[GOAL]
case h
ι : Sort u_1
α : Type u
β : Type v
inst✝¹ : PseudoEMetricSpace α
δ✝ : ℝ
s : Set α
x✝¹ : α
X : Type u
inst✝ : PseudoMetricSpace X
δ : ℝ
x x✝ : X
⊢ x✝ ∈ thickening δ {x} ↔ x✝ ∈ ball x δ
[PROOFSTEP]
simp [mem_thickening_iff]
[GOAL]
ι : Sort u_1
α : Type u
β : Type v
inst✝¹ : PseudoEMetricSpace α
δ✝ : ℝ
s : Set α
x✝ : α
X : Type u
inst✝ : PseudoMetricSpace X
x : X
E : Set X
hx : x ∈ E
δ : ℝ
⊢ ball x δ ⊆ thickening δ {x}
[PROOFSTEP]
simp [Subset.rfl]
[GOAL]
ι : Sort u_1
α : Type u
β : Type v
inst✝¹ : PseudoEMetricSpace α
δ✝ : ℝ
s : Set α
x : α
X : Type u
inst✝ : PseudoMetricSpace X
δ : ℝ
E : Set X
⊢ thickening δ E = ⋃ (x : X) (_ : x ∈ E), ball x δ
[PROOFSTEP]
ext x
[GOAL]
case h
ι : Sort u_1
α : Type u
β : Type v
inst✝¹ : PseudoEMetricSpace α
δ✝ : ℝ
s : Set α
x✝ : α
X : Type u
inst✝ : PseudoMetricSpace X
δ : ℝ
E : Set X
x : X
⊢ x ∈ thickening δ E ↔ x ∈ ⋃ (x : X) (_ : x ∈ E), ball x δ
[PROOFSTEP]
simp only [mem_iUnion₂, exists_prop]
[GOAL]
case h
ι : Sort u_1
α : Type u
β : Type v
inst✝¹ : PseudoEMetricSpace α
δ✝ : ℝ
s : Set α
x✝ : α
X : Type u
inst✝ : PseudoMetricSpace X
δ : ℝ
E : Set X
x : X
⊢ x ∈ thickening δ E ↔ ∃ i, i ∈ E ∧ x ∈ ball i δ
[PROOFSTEP]
exact mem_thickening_iff
[GOAL]
ι : Sort u_1
α : Type u
β : Type v
inst✝¹ : PseudoEMetricSpace α
δ✝ : ℝ
s : Set α
x : α
X : Type u
inst✝ : PseudoMetricSpace X
δ : ℝ
E : Set X
h : Bounded E
⊢ Bounded (thickening δ E)
[PROOFSTEP]
rcases E.eq_empty_or_nonempty with rfl | ⟨x, hx⟩
[GOAL]
case inl
ι : Sort u_1
α : Type u
β : Type v
inst✝¹ : PseudoEMetricSpace α
δ✝ : ℝ
s : Set α
x : α
X : Type u
inst✝ : PseudoMetricSpace X
δ : ℝ
h : Bounded ∅
⊢ Bounded (thickening δ ∅)
[PROOFSTEP]
simp
[GOAL]
case inr.intro
ι : Sort u_1
α : Type u
β : Type v
inst✝¹ : PseudoEMetricSpace α
δ✝ : ℝ
s : Set α
x✝ : α
X : Type u
inst✝ : PseudoMetricSpace X
δ : ℝ
E : Set X
h : Bounded E
x : X
hx : x ∈ E
⊢ Bounded (thickening δ E)
[PROOFSTEP]
refine (bounded_iff_subset_ball x).2 ⟨δ + diam E, fun y hy ↦ ?_⟩
[GOAL]
case inr.intro
ι : Sort u_1
α : Type u
β : Type v
inst✝¹ : PseudoEMetricSpace α
δ✝ : ℝ
s : Set α
x✝ : α
X : Type u
inst✝ : PseudoMetricSpace X
δ : ℝ
E : Set X
h : Bounded E
x : X
hx : x ∈ E
y : X
hy : y ∈ thickening δ E
⊢ y ∈ closedBall x (δ + diam E)
[PROOFSTEP]
calc
  dist y x ≤ infDist y E + diam E := dist_le_infDist_add_diam (x := y) h hx
  _ ≤ δ + diam E := add_le_add_right ((mem_thickening_iff_infDist_lt ⟨x, hx⟩).1 hy).le _
[GOAL]
ι : Sort u_1
α : Type u
β : Type v
inst✝ : PseudoEMetricSpace α
δ ε : ℝ
s t : Set α
x✝ : α
E : Set α
x : α
h : ¬x ∈ closure E
⊢ ∀ᶠ (δ : ℝ) in 𝓝 0, ¬x ∈ cthickening δ E
[PROOFSTEP]
obtain ⟨ε, ⟨ε_pos, ε_lt⟩⟩ := exists_real_pos_lt_infEdist_of_not_mem_closure h
[GOAL]
case intro.intro
ι : Sort u_1
α : Type u
β : Type v
inst✝ : PseudoEMetricSpace α
δ ε✝ : ℝ
s t : Set α
x✝ : α
E : Set α
x : α
h : ¬x ∈ closure E
ε : ℝ
ε_pos : 0 < ε
ε_lt : ENNReal.ofReal ε < infEdist x E
⊢ ∀ᶠ (δ : ℝ) in 𝓝 0, ¬x ∈ cthickening δ E
[PROOFSTEP]
filter_upwards [eventually_lt_nhds ε_pos] with δ hδ
[GOAL]
case h
ι : Sort u_1
α : Type u
β : Type v
inst✝ : PseudoEMetricSpace α
δ✝ ε✝ : ℝ
s t : Set α
x✝ : α
E : Set α
x : α
h : ¬x ∈ closure E
ε : ℝ
ε_pos : 0 < ε
ε_lt : ENNReal.ofReal ε < infEdist x E
δ : ℝ
hδ : δ < ε
⊢ ¬x ∈ cthickening δ E
[PROOFSTEP]
simp only [cthickening, mem_setOf_eq, not_le]
[GOAL]
case h
ι : Sort u_1
α : Type u
β : Type v
inst✝ : PseudoEMetricSpace α
δ✝ ε✝ : ℝ
s t : Set α
x✝ : α
E : Set α
x : α
h : ¬x ∈ closure E
ε : ℝ
ε_pos : 0 < ε
ε_lt : ENNReal.ofReal ε < infEdist x E
δ : ℝ
hδ : δ < ε
⊢ ENNReal.ofReal δ < infEdist x E
[PROOFSTEP]
exact ((ofReal_lt_ofReal_iff ε_pos).mpr hδ).trans ε_lt
[GOAL]
ι : Sort u_1
α✝ : Type u
β : Type v
inst✝¹ : PseudoEMetricSpace α✝
δ✝ ε : ℝ
s t : Set α✝
x✝ : α✝
α : Type u_2
inst✝ : PseudoMetricSpace α
x y : α
δ : ℝ
E : Set α
h : y ∈ E
h' : dist x y ≤ δ
⊢ x ∈ cthickening δ E
[PROOFSTEP]
apply mem_cthickening_of_edist_le x y δ E h
[GOAL]
ι : Sort u_1
α✝ : Type u
β : Type v
inst✝¹ : PseudoEMetricSpace α✝
δ✝ ε : ℝ
s t : Set α✝
x✝ : α✝
α : Type u_2
inst✝ : PseudoMetricSpace α
x y : α
δ : ℝ
E : Set α
h : y ∈ E
h' : dist x y ≤ δ
⊢ edist x y ≤ ENNReal.ofReal δ
[PROOFSTEP]
rw [edist_dist]
[GOAL]
ι : Sort u_1
α✝ : Type u
β : Type v
inst✝¹ : PseudoEMetricSpace α✝
δ✝ ε : ℝ
s t : Set α✝
x✝ : α✝
α : Type u_2
inst✝ : PseudoMetricSpace α
x y : α
δ : ℝ
E : Set α
h : y ∈ E
h' : dist x y ≤ δ
⊢ ENNReal.ofReal (dist x y) ≤ ENNReal.ofReal δ
[PROOFSTEP]
exact ENNReal.ofReal_le_ofReal h'
[GOAL]
ι : Sort u_1
α : Type u
β : Type v
inst✝ : PseudoEMetricSpace α
δ✝ ε : ℝ
s t : Set α
x : α
δ : ℝ
⊢ cthickening δ ∅ = ∅
[PROOFSTEP]
simp only [cthickening, ENNReal.ofReal_ne_top, setOf_false, infEdist_empty, top_le_iff]
[GOAL]
ι : Sort u_1
α : Type u
β : Type v
inst✝ : PseudoEMetricSpace α
δ✝ ε : ℝ
s t : Set α
x : α
δ : ℝ
hδ : δ ≤ 0
E : Set α
⊢ cthickening δ E = closure E
[PROOFSTEP]
ext x
[GOAL]
case h
ι : Sort u_1
α : Type u
β : Type v
inst✝ : PseudoEMetricSpace α
δ✝ ε : ℝ
s t : Set α
x✝ : α
δ : ℝ
hδ : δ ≤ 0
E : Set α
x : α
⊢ x ∈ cthickening δ E ↔ x ∈ closure E
[PROOFSTEP]
simp [mem_closure_iff_infEdist_zero, cthickening, ENNReal.ofReal_eq_zero.2 hδ]
[GOAL]
ι : Sort u_1
α : Type u
β : Type v
inst✝ : PseudoEMetricSpace α
δ✝ ε : ℝ
s t : Set α
x : α
δ : ℝ
E : Set α
⊢ cthickening (max 0 δ) E = cthickening δ E
[PROOFSTEP]
cases le_total δ 0
[GOAL]
case inl
ι : Sort u_1
α : Type u
β : Type v
inst✝ : PseudoEMetricSpace α
δ✝ ε : ℝ
s t : Set α
x : α
δ : ℝ
E : Set α
h✝ : δ ≤ 0
⊢ cthickening (max 0 δ) E = cthickening δ E
[PROOFSTEP]
simp [cthickening_of_nonpos, *]
[GOAL]
case inr
ι : Sort u_1
α : Type u
β : Type v
inst✝ : PseudoEMetricSpace α
δ✝ ε : ℝ
s t : Set α
x : α
δ : ℝ
E : Set α
h✝ : 0 ≤ δ
⊢ cthickening (max 0 δ) E = cthickening δ E
[PROOFSTEP]
simp [cthickening_of_nonpos, *]
[GOAL]
ι : Sort u_1
α✝ : Type u
β : Type v
inst✝¹ : PseudoEMetricSpace α✝
δ✝ ε : ℝ
s t : Set α✝
x✝ : α✝
α : Type u_2
inst✝ : PseudoMetricSpace α
x : α
δ : ℝ
hδ : 0 ≤ δ
⊢ cthickening δ {x} = closedBall x δ
[PROOFSTEP]
ext y
[GOAL]
case h
ι : Sort u_1
α✝ : Type u
β : Type v
inst✝¹ : PseudoEMetricSpace α✝
δ✝ ε : ℝ
s t : Set α✝
x✝ : α✝
α : Type u_2
inst✝ : PseudoMetricSpace α
x : α
δ : ℝ
hδ : 0 ≤ δ
y : α
⊢ y ∈ cthickening δ {x} ↔ y ∈ closedBall x δ
[PROOFSTEP]
simp [cthickening, edist_dist, ENNReal.ofReal_le_ofReal_iff hδ]
[GOAL]
ι : Sort u_1
α✝ : Type u
β : Type v
inst✝¹ : PseudoEMetricSpace α✝
δ✝ ε : ℝ
s t : Set α✝
x✝ : α✝
α : Type u_2
inst✝ : PseudoMetricSpace α
x : α
δ : ℝ
⊢ closedBall x δ ⊆ cthickening δ {x}
[PROOFSTEP]
rcases lt_or_le δ 0 with (hδ | hδ)
[GOAL]
case inl
ι : Sort u_1
α✝ : Type u
β : Type v
inst✝¹ : PseudoEMetricSpace α✝
δ✝ ε : ℝ
s t : Set α✝
x✝ : α✝
α : Type u_2
inst✝ : PseudoMetricSpace α
x : α
δ : ℝ
hδ : δ < 0
⊢ closedBall x δ ⊆ cthickening δ {x}
[PROOFSTEP]
simp only [closedBall_eq_empty.mpr hδ, empty_subset]
[GOAL]
case inr
ι : Sort u_1
α✝ : Type u
β : Type v
inst✝¹ : PseudoEMetricSpace α✝
δ✝ ε : ℝ
s t : Set α✝
x✝ : α✝
α : Type u_2
inst✝ : PseudoMetricSpace α
x : α
δ : ℝ
hδ : 0 ≤ δ
⊢ closedBall x δ ⊆ cthickening δ {x}
[PROOFSTEP]
simp only [cthickening_singleton x hδ, Subset.rfl]
[GOAL]
ι : Sort u_1
α : Type u
β : Type v
inst✝ : PseudoEMetricSpace α
δ✝ ε : ℝ
s t : Set α
x : α
δ : ℝ
E : Set α
⊢ thickening δ E ⊆ cthickening δ E
[PROOFSTEP]
intro x hx
[GOAL]
ι : Sort u_1
α : Type u
β : Type v
inst✝ : PseudoEMetricSpace α
δ✝ ε : ℝ
s t : Set α
x✝ : α
δ : ℝ
E : Set α
x : α
hx : x ∈ thickening δ E
⊢ x ∈ cthickening δ E
[PROOFSTEP]
rw [thickening, mem_setOf_eq] at hx 
[GOAL]
ι : Sort u_1
α : Type u
β : Type v
inst✝ : PseudoEMetricSpace α
δ✝ ε : ℝ
s t : Set α
x✝ : α
δ : ℝ
E : Set α
x : α
hx : infEdist x E < ENNReal.ofReal δ
⊢ x ∈ cthickening δ E
[PROOFSTEP]
exact hx.le
[GOAL]
ι : Sort u_1
α✝ : Type u
β : Type v
inst✝¹ : PseudoEMetricSpace α✝
δ✝ ε : ℝ
s t : Set α✝
x : α✝
α : Type u_2
inst✝ : PseudoMetricSpace α
δ : ℝ
E : Set α
h : Bounded E
⊢ Bounded (Metric.cthickening δ E)
[PROOFSTEP]
have : Bounded (thickening (max (δ + 1) 1) E) := h.thickening
[GOAL]
ι : Sort u_1
α✝ : Type u
β : Type v
inst✝¹ : PseudoEMetricSpace α✝
δ✝ ε : ℝ
s t : Set α✝
x : α✝
α : Type u_2
inst✝ : PseudoMetricSpace α
δ : ℝ
E : Set α
h : Bounded E
this : Bounded (thickening (max (δ + 1) 1) E)
⊢ Bounded (Metric.cthickening δ E)
[PROOFSTEP]
apply Bounded.mono _ this
[GOAL]
ι : Sort u_1
α✝ : Type u
β : Type v
inst✝¹ : PseudoEMetricSpace α✝
δ✝ ε : ℝ
s t : Set α✝
x : α✝
α : Type u_2
inst✝ : PseudoMetricSpace α
δ : ℝ
E : Set α
h : Bounded E
this : Bounded (thickening (max (δ + 1) 1) E)
⊢ Metric.cthickening δ E ⊆ thickening (max (δ + 1) 1) E
[PROOFSTEP]
exact
  cthickening_subset_thickening' (zero_lt_one.trans_le (le_max_right _ _)) ((lt_add_one _).trans_le (le_max_left _ _)) _
[GOAL]
ι : Sort u_1
α : Type u
β : Type v
inst✝ : PseudoEMetricSpace α
δ✝ ε : ℝ
s t : Set α
x : α
δ : ℝ
E : Set α
⊢ closure E ⊆ cthickening δ E
[PROOFSTEP]
rw [← cthickening_of_nonpos (min_le_right δ 0)]
[GOAL]
ι : Sort u_1
α : Type u
β : Type v
inst✝ : PseudoEMetricSpace α
δ✝ ε : ℝ
s t : Set α
x : α
δ : ℝ
E : Set α
⊢ cthickening (min δ 0) E ⊆ cthickening δ E
[PROOFSTEP]
exact cthickening_mono (min_le_left δ 0) E
[GOAL]
ι : Sort u_1
α : Type u
β : Type v
inst✝ : PseudoEMetricSpace α
δ✝ ε : ℝ
s t : Set α
x : α
δ : ℝ
δ_pos : 0 < δ
E : Set α
⊢ closure E ⊆ thickening δ E
[PROOFSTEP]
rw [← cthickening_zero]
[GOAL]
ι : Sort u_1
α : Type u
β : Type v
inst✝ : PseudoEMetricSpace α
δ✝ ε : ℝ
s t : Set α
x : α
δ : ℝ
δ_pos : 0 < δ
E : Set α
⊢ cthickening 0 E ⊆ thickening δ E
[PROOFSTEP]
exact cthickening_subset_thickening' δ_pos δ_pos E
[GOAL]
ι : Sort u_1
α : Type u
β : Type v
inst✝ : PseudoEMetricSpace α
δ✝ ε : ℝ
s✝ t✝ : Set α
x : α
δ : ℝ
s t : Set α
⊢ thickening δ (s ∪ t) = thickening δ s ∪ thickening δ t
[PROOFSTEP]
simp_rw [thickening, infEdist_union, inf_eq_min, min_lt_iff, setOf_or]
[GOAL]
ι : Sort u_1
α : Type u
β : Type v
inst✝ : PseudoEMetricSpace α
δ✝ ε : ℝ
s✝ t✝ : Set α
x : α
δ : ℝ
s t : Set α
⊢ cthickening δ (s ∪ t) = cthickening δ s ∪ cthickening δ t
[PROOFSTEP]
simp_rw [cthickening, infEdist_union, inf_eq_min, min_le_iff, setOf_or]
[GOAL]
ι : Sort u_1
α : Type u
β : Type v
inst✝ : PseudoEMetricSpace α
δ✝ ε : ℝ
s t : Set α
x : α
δ : ℝ
f : ι → Set α
⊢ thickening δ (⋃ (i : ι), f i) = ⋃ (i : ι), thickening δ (f i)
[PROOFSTEP]
simp_rw [thickening, infEdist_iUnion, iInf_lt_iff, setOf_exists]
[GOAL]
ι : Sort u_1
α : Type u
β : Type v
inst✝ : PseudoEMetricSpace α
δ ε✝ : ℝ
s t : Set α
x : α
ε : ℝ≥0
⊢ EMetric.diam (cthickening (↑ε) s) ≤ EMetric.diam s + 2 * ↑ε
[PROOFSTEP]
refine' diam_le fun x hx y hy => ENNReal.le_of_forall_pos_le_add fun δ hδ _ => _
[GOAL]
ι : Sort u_1
α : Type u
β : Type v
inst✝ : PseudoEMetricSpace α
δ✝ ε✝ : ℝ
s t : Set α
x✝¹ : α
ε : ℝ≥0
x : α
hx : x ∈ cthickening (↑ε) s
y : α
hy : y ∈ cthickening (↑ε) s
δ : ℝ≥0
hδ : 0 < δ
x✝ : EMetric.diam s + 2 * ↑ε < ⊤
⊢ edist x y ≤ EMetric.diam s + 2 * ↑ε + ↑δ
[PROOFSTEP]
rw [mem_cthickening_iff, ENNReal.ofReal_coe_nnreal] at hx hy 
[GOAL]
ι : Sort u_1
α : Type u
β : Type v
inst✝ : PseudoEMetricSpace α
δ✝ ε✝ : ℝ
s t : Set α
x✝¹ : α
ε : ℝ≥0
x : α
hx : infEdist x s ≤ ↑ε
y : α
hy : infEdist y s ≤ ↑ε
δ : ℝ≥0
hδ : 0 < δ
x✝ : EMetric.diam s + 2 * ↑ε < ⊤
⊢ edist x y ≤ EMetric.diam s + 2 * ↑ε + ↑δ
[PROOFSTEP]
have hε : (ε : ℝ≥0∞) < ε + δ := ENNReal.coe_lt_coe.2 (lt_add_of_pos_right _ hδ)
[GOAL]
ι : Sort u_1
α : Type u
β : Type v
inst✝ : PseudoEMetricSpace α
δ✝ ε✝ : ℝ
s t : Set α
x✝¹ : α
ε : ℝ≥0
x : α
hx : infEdist x s ≤ ↑ε
y : α
hy : infEdist y s ≤ ↑ε
δ : ℝ≥0
hδ : 0 < δ
x✝ : EMetric.diam s + 2 * ↑ε < ⊤
hε : ↑ε < ↑ε + ↑δ
⊢ edist x y ≤ EMetric.diam s + 2 * ↑ε + ↑δ
[PROOFSTEP]
replace hx := hx.trans_lt hε
[GOAL]
ι : Sort u_1
α : Type u
β : Type v
inst✝ : PseudoEMetricSpace α
δ✝ ε✝ : ℝ
s t : Set α
x✝¹ : α
ε : ℝ≥0
x y : α
hy : infEdist y s ≤ ↑ε
δ : ℝ≥0
hδ : 0 < δ
x✝ : EMetric.diam s + 2 * ↑ε < ⊤
hε : ↑ε < ↑ε + ↑δ
hx : infEdist x s < ↑ε + ↑δ
⊢ edist x y ≤ EMetric.diam s + 2 * ↑ε + ↑δ
[PROOFSTEP]
obtain ⟨x', hx', hxx'⟩ := infEdist_lt_iff.mp hx
[GOAL]
case intro.intro
ι : Sort u_1
α : Type u
β : Type v
inst✝ : PseudoEMetricSpace α
δ✝ ε✝ : ℝ
s t : Set α
x✝¹ : α
ε : ℝ≥0
x y : α
hy : infEdist y s ≤ ↑ε
δ : ℝ≥0
hδ : 0 < δ
x✝ : EMetric.diam s + 2 * ↑ε < ⊤
hε : ↑ε < ↑ε + ↑δ
hx : infEdist x s < ↑ε + ↑δ
x' : α
hx' : x' ∈ s
hxx' : edist x x' < ↑ε + ↑δ
⊢ edist x y ≤ EMetric.diam s + 2 * ↑ε + ↑δ
[PROOFSTEP]
calc
  edist x y ≤ edist x x' + edist y x' := edist_triangle_right _ _ _
  _ ≤ ε + δ + (infEdist y s + EMetric.diam s) := (add_le_add hxx'.le (edist_le_infEdist_add_ediam hx'))
  _ ≤ ε + δ + (ε + EMetric.diam s) := (add_le_add_left (add_le_add_right hy _) _)
  _ = _ := by rw [two_mul]; ac_rfl
[GOAL]
ι : Sort u_1
α : Type u
β : Type v
inst✝ : PseudoEMetricSpace α
δ✝ ε✝ : ℝ
s t : Set α
x✝¹ : α
ε : ℝ≥0
x y : α
hy : infEdist y s ≤ ↑ε
δ : ℝ≥0
hδ : 0 < δ
x✝ : EMetric.diam s + 2 * ↑ε < ⊤
hε : ↑ε < ↑ε + ↑δ
hx : infEdist x s < ↑ε + ↑δ
x' : α
hx' : x' ∈ s
hxx' : edist x x' < ↑ε + ↑δ
⊢ ↑ε + ↑δ + (↑ε + EMetric.diam s) = EMetric.diam s + 2 * ↑ε + ↑δ
[PROOFSTEP]
rw [two_mul]
[GOAL]
ι : Sort u_1
α : Type u
β : Type v
inst✝ : PseudoEMetricSpace α
δ✝ ε✝ : ℝ
s t : Set α
x✝¹ : α
ε : ℝ≥0
x y : α
hy : infEdist y s ≤ ↑ε
δ : ℝ≥0
hδ : 0 < δ
x✝ : EMetric.diam s + 2 * ↑ε < ⊤
hε : ↑ε < ↑ε + ↑δ
hx : infEdist x s < ↑ε + ↑δ
x' : α
hx' : x' ∈ s
hxx' : edist x x' < ↑ε + ↑δ
⊢ ↑ε + ↑δ + (↑ε + EMetric.diam s) = EMetric.diam s + (↑ε + ↑ε) + ↑δ
[PROOFSTEP]
ac_rfl
[GOAL]
ι : Sort u_1
α✝ : Type u
β : Type v
inst✝¹ : PseudoEMetricSpace α✝
δ ε : ℝ
s✝ t : Set α✝
x : α✝
α : Type u_2
inst✝ : PseudoMetricSpace α
s : Set α
hε : 0 ≤ ε
⊢ diam (cthickening ε s) ≤ diam s + 2 * ε
[PROOFSTEP]
lift ε to ℝ≥0 using hε
[GOAL]
case intro
ι : Sort u_1
α✝ : Type u
β : Type v
inst✝¹ : PseudoEMetricSpace α✝
δ : ℝ
s✝ t : Set α✝
x : α✝
α : Type u_2
inst✝ : PseudoMetricSpace α
s : Set α
ε : ℝ≥0
⊢ diam (cthickening (↑ε) s) ≤ diam s + 2 * ↑ε
[PROOFSTEP]
refine (toReal_le_add' (ediam_cthickening_le _) ?_ ?_).trans_eq ?_
[GOAL]
case intro.refine_1
ι : Sort u_1
α✝ : Type u
β : Type v
inst✝¹ : PseudoEMetricSpace α✝
δ : ℝ
s✝ t : Set α✝
x : α✝
α : Type u_2
inst✝ : PseudoMetricSpace α
s : Set α
ε : ℝ≥0
⊢ EMetric.diam s = ⊤ → EMetric.diam (cthickening (↑ε) s) = ⊤
[PROOFSTEP]
exact fun h ↦ top_unique <| h ▸ EMetric.diam_mono (self_subset_cthickening _)
[GOAL]
case intro.refine_2
ι : Sort u_1
α✝ : Type u
β : Type v
inst✝¹ : PseudoEMetricSpace α✝
δ : ℝ
s✝ t : Set α✝
x : α✝
α : Type u_2
inst✝ : PseudoMetricSpace α
s : Set α
ε : ℝ≥0
⊢ 2 * ↑ε = ⊤ → EMetric.diam (cthickening (↑ε) s) = ⊤
[PROOFSTEP]
simp [mul_eq_top]
[GOAL]
case intro.refine_3
ι : Sort u_1
α✝ : Type u
β : Type v
inst✝¹ : PseudoEMetricSpace α✝
δ : ℝ
s✝ t : Set α✝
x : α✝
α : Type u_2
inst✝ : PseudoMetricSpace α
s : Set α
ε : ℝ≥0
⊢ ENNReal.toReal (EMetric.diam s) + ENNReal.toReal (2 * ↑ε) = diam s + 2 * ↑ε
[PROOFSTEP]
simp [diam]
[GOAL]
ι : Sort u_1
α✝ : Type u
β : Type v
inst✝¹ : PseudoEMetricSpace α✝
δ ε : ℝ
s✝ t : Set α✝
x : α✝
α : Type u_2
inst✝ : PseudoMetricSpace α
s : Set α
hε : 0 ≤ ε
⊢ diam (thickening ε s) ≤ diam s + 2 * ε
[PROOFSTEP]
by_cases hs : Bounded s
[GOAL]
case pos
ι : Sort u_1
α✝ : Type u
β : Type v
inst✝¹ : PseudoEMetricSpace α✝
δ ε : ℝ
s✝ t : Set α✝
x : α✝
α : Type u_2
inst✝ : PseudoMetricSpace α
s : Set α
hε : 0 ≤ ε
hs : Bounded s
⊢ diam (thickening ε s) ≤ diam s + 2 * ε
[PROOFSTEP]
exact (diam_mono (thickening_subset_cthickening _ _) hs.cthickening).trans (diam_cthickening_le _ hε)
[GOAL]
case neg
ι : Sort u_1
α✝ : Type u
β : Type v
inst✝¹ : PseudoEMetricSpace α✝
δ ε : ℝ
s✝ t : Set α✝
x : α✝
α : Type u_2
inst✝ : PseudoMetricSpace α
s : Set α
hε : 0 ≤ ε
hs : ¬Bounded s
⊢ diam (thickening ε s) ≤ diam s + 2 * ε
[PROOFSTEP]
obtain rfl | hε := hε.eq_or_lt
[GOAL]
case neg.inl
ι : Sort u_1
α✝ : Type u
β : Type v
inst✝¹ : PseudoEMetricSpace α✝
δ : ℝ
s✝ t : Set α✝
x : α✝
α : Type u_2
inst✝ : PseudoMetricSpace α
s : Set α
hs : ¬Bounded s
hε : 0 ≤ 0
⊢ diam (thickening 0 s) ≤ diam s + 2 * 0
[PROOFSTEP]
simp [thickening_of_nonpos, diam_nonneg]
[GOAL]
case neg.inr
ι : Sort u_1
α✝ : Type u
β : Type v
inst✝¹ : PseudoEMetricSpace α✝
δ ε : ℝ
s✝ t : Set α✝
x : α✝
α : Type u_2
inst✝ : PseudoMetricSpace α
s : Set α
hε✝ : 0 ≤ ε
hs : ¬Bounded s
hε : 0 < ε
⊢ diam (thickening ε s) ≤ diam s + 2 * ε
[PROOFSTEP]
rw [diam_eq_zero_of_unbounded (mt (Bounded.mono <| self_subset_thickening hε _) hs)]
[GOAL]
case neg.inr
ι : Sort u_1
α✝ : Type u
β : Type v
inst✝¹ : PseudoEMetricSpace α✝
δ ε : ℝ
s✝ t : Set α✝
x : α✝
α : Type u_2
inst✝ : PseudoMetricSpace α
s : Set α
hε✝ : 0 ≤ ε
hs : ¬Bounded s
hε : 0 < ε
⊢ 0 ≤ diam s + 2 * ε
[PROOFSTEP]
positivity
[GOAL]
ι : Sort u_1
α : Type u
β : Type v
inst✝ : PseudoEMetricSpace α
δ ε : ℝ
s t : Set α
x : α
⊢ thickening δ (closure s) = thickening δ s
[PROOFSTEP]
simp_rw [thickening, infEdist_closure]
[GOAL]
ι : Sort u_1
α : Type u
β : Type v
inst✝ : PseudoEMetricSpace α
δ ε : ℝ
s t : Set α
x : α
⊢ cthickening δ (closure s) = cthickening δ s
[PROOFSTEP]
simp_rw [cthickening, infEdist_closure]
[GOAL]
ι : Sort u_1
α : Type u
β : Type v
inst✝ : PseudoEMetricSpace α
δ ε : ℝ
s t : Set α
x : α
hst : Disjoint s t
hs : IsCompact s
ht : IsClosed t
⊢ ∃ δ, 0 < δ ∧ Disjoint (thickening δ s) (thickening δ t)
[PROOFSTEP]
obtain ⟨r, hr, h⟩ := exists_pos_forall_lt_edist hs ht hst
[GOAL]
case intro.intro
ι : Sort u_1
α : Type u
β : Type v
inst✝ : PseudoEMetricSpace α
δ ε : ℝ
s t : Set α
x : α
hst : Disjoint s t
hs : IsCompact s
ht : IsClosed t
r : ℝ≥0
hr : 0 < r
h : ∀ (x : α), x ∈ s → ∀ (y : α), y ∈ t → ↑r < edist x y
⊢ ∃ δ, 0 < δ ∧ Disjoint (thickening δ s) (thickening δ t)
[PROOFSTEP]
refine' ⟨r / 2, half_pos (NNReal.coe_pos.2 hr), _⟩
[GOAL]
case intro.intro
ι : Sort u_1
α : Type u
β : Type v
inst✝ : PseudoEMetricSpace α
δ ε : ℝ
s t : Set α
x : α
hst : Disjoint s t
hs : IsCompact s
ht : IsClosed t
r : ℝ≥0
hr : 0 < r
h : ∀ (x : α), x ∈ s → ∀ (y : α), y ∈ t → ↑r < edist x y
⊢ Disjoint (thickening (↑r / 2) s) (thickening (↑r / 2) t)
[PROOFSTEP]
rw [disjoint_iff_inf_le]
[GOAL]
case intro.intro
ι : Sort u_1
α : Type u
β : Type v
inst✝ : PseudoEMetricSpace α
δ ε : ℝ
s t : Set α
x : α
hst : Disjoint s t
hs : IsCompact s
ht : IsClosed t
r : ℝ≥0
hr : 0 < r
h : ∀ (x : α), x ∈ s → ∀ (y : α), y ∈ t → ↑r < edist x y
⊢ thickening (↑r / 2) s ⊓ thickening (↑r / 2) t ≤ ⊥
[PROOFSTEP]
rintro z ⟨hzs, hzt⟩
[GOAL]
case intro.intro.intro
ι : Sort u_1
α : Type u
β : Type v
inst✝ : PseudoEMetricSpace α
δ ε : ℝ
s t : Set α
x : α
hst : Disjoint s t
hs : IsCompact s
ht : IsClosed t
r : ℝ≥0
hr : 0 < r
h : ∀ (x : α), x ∈ s → ∀ (y : α), y ∈ t → ↑r < edist x y
z : α
hzs : z ∈ thickening (↑r / 2) s
hzt : z ∈ thickening (↑r / 2) t
⊢ z ∈ ⊥
[PROOFSTEP]
rw [mem_thickening_iff_exists_edist_lt] at hzs hzt 
[GOAL]
case intro.intro.intro
ι : Sort u_1
α : Type u
β : Type v
inst✝ : PseudoEMetricSpace α
δ ε : ℝ
s t : Set α
x : α
hst : Disjoint s t
hs : IsCompact s
ht : IsClosed t
r : ℝ≥0
hr : 0 < r
h : ∀ (x : α), x ∈ s → ∀ (y : α), y ∈ t → ↑r < edist x y
z : α
hzs : ∃ z_1, z_1 ∈ s ∧ edist z z_1 < ENNReal.ofReal (↑r / 2)
hzt : ∃ z_1, z_1 ∈ t ∧ edist z z_1 < ENNReal.ofReal (↑r / 2)
⊢ z ∈ ⊥
[PROOFSTEP]
rw [← NNReal.coe_two, ← NNReal.coe_div, ENNReal.ofReal_coe_nnreal] at hzs hzt 
[GOAL]
case intro.intro.intro
ι : Sort u_1
α : Type u
β : Type v
inst✝ : PseudoEMetricSpace α
δ ε : ℝ
s t : Set α
x : α
hst : Disjoint s t
hs : IsCompact s
ht : IsClosed t
r : ℝ≥0
hr : 0 < r
h : ∀ (x : α), x ∈ s → ∀ (y : α), y ∈ t → ↑r < edist x y
z : α
hzs : ∃ z_1, z_1 ∈ s ∧ edist z z_1 < ↑(r / 2)
hzt : ∃ z_1, z_1 ∈ t ∧ edist z z_1 < ↑(r / 2)
⊢ z ∈ ⊥
[PROOFSTEP]
obtain ⟨x, hx, hzx⟩ := hzs
[GOAL]
case intro.intro.intro.intro.intro
ι : Sort u_1
α : Type u
β : Type v
inst✝ : PseudoEMetricSpace α
δ ε : ℝ
s t : Set α
x✝ : α
hst : Disjoint s t
hs : IsCompact s
ht : IsClosed t
r : ℝ≥0
hr : 0 < r
h : ∀ (x : α), x ∈ s → ∀ (y : α), y ∈ t → ↑r < edist x y
z : α
hzt : ∃ z_1, z_1 ∈ t ∧ edist z z_1 < ↑(r / 2)
x : α
hx : x ∈ s
hzx : edist z x < ↑(r / 2)
⊢ z ∈ ⊥
[PROOFSTEP]
obtain ⟨y, hy, hzy⟩ := hzt
[GOAL]
case intro.intro.intro.intro.intro.intro.intro
ι : Sort u_1
α : Type u
β : Type v
inst✝ : PseudoEMetricSpace α
δ ε : ℝ
s t : Set α
x✝ : α
hst : Disjoint s t
hs : IsCompact s
ht : IsClosed t
r : ℝ≥0
hr : 0 < r
h : ∀ (x : α), x ∈ s → ∀ (y : α), y ∈ t → ↑r < edist x y
z x : α
hx : x ∈ s
hzx : edist z x < ↑(r / 2)
y : α
hy : y ∈ t
hzy : edist z y < ↑(r / 2)
⊢ z ∈ ⊥
[PROOFSTEP]
refine' (h x hx y hy).not_le _
[GOAL]
case intro.intro.intro.intro.intro.intro.intro
ι : Sort u_1
α : Type u
β : Type v
inst✝ : PseudoEMetricSpace α
δ ε : ℝ
s t : Set α
x✝ : α
hst : Disjoint s t
hs : IsCompact s
ht : IsClosed t
r : ℝ≥0
hr : 0 < r
h : ∀ (x : α), x ∈ s → ∀ (y : α), y ∈ t → ↑r < edist x y
z x : α
hx : x ∈ s
hzx : edist z x < ↑(r / 2)
y : α
hy : y ∈ t
hzy : edist z y < ↑(r / 2)
⊢ edist x y ≤ ↑r
[PROOFSTEP]
calc
  edist x y ≤ edist z x + edist z y := edist_triangle_left _ _ _
  _ ≤ ↑(r / 2) + ↑(r / 2) := (add_le_add hzx.le hzy.le)
  _ = r := by rw [← ENNReal.coe_add, add_halves]
[GOAL]
ι : Sort u_1
α : Type u
β : Type v
inst✝ : PseudoEMetricSpace α
δ ε : ℝ
s t : Set α
x✝ : α
hst : Disjoint s t
hs : IsCompact s
ht : IsClosed t
r : ℝ≥0
hr : 0 < r
h : ∀ (x : α), x ∈ s → ∀ (y : α), y ∈ t → ↑r < edist x y
z x : α
hx : x ∈ s
hzx : edist z x < ↑(r / 2)
y : α
hy : y ∈ t
hzy : edist z y < ↑(r / 2)
⊢ ↑(r / 2) + ↑(r / 2) = ↑r
[PROOFSTEP]
rw [← ENNReal.coe_add, add_halves]
[GOAL]
ι : Sort u_1
α : Type u
β : Type v
inst✝ : PseudoEMetricSpace α
δ ε : ℝ
s t : Set α
x : α
hst : Disjoint s t
hs : IsCompact s
ht : IsClosed t
⊢ ∃ δ, 0 < δ ∧ Disjoint (cthickening δ s) (cthickening δ t)
[PROOFSTEP]
obtain ⟨δ, hδ, h⟩ := hst.exists_thickenings hs ht
[GOAL]
case intro.intro
ι : Sort u_1
α : Type u
β : Type v
inst✝ : PseudoEMetricSpace α
δ✝ ε : ℝ
s t : Set α
x : α
hst : Disjoint s t
hs : IsCompact s
ht : IsClosed t
δ : ℝ
hδ : 0 < δ
h : Disjoint (thickening δ s) (thickening δ t)
⊢ ∃ δ, 0 < δ ∧ Disjoint (cthickening δ s) (cthickening δ t)
[PROOFSTEP]
refine' ⟨δ / 2, half_pos hδ, h.mono _ _⟩
[GOAL]
case intro.intro.refine'_1
ι : Sort u_1
α : Type u
β : Type v
inst✝ : PseudoEMetricSpace α
δ✝ ε : ℝ
s t : Set α
x : α
hst : Disjoint s t
hs : IsCompact s
ht : IsClosed t
δ : ℝ
hδ : 0 < δ
h : Disjoint (thickening δ s) (thickening δ t)
⊢ cthickening (δ / 2) s ≤ thickening δ s
[PROOFSTEP]
exact cthickening_subset_thickening' hδ (half_lt_self hδ) _
[GOAL]
case intro.intro.refine'_2
ι : Sort u_1
α : Type u
β : Type v
inst✝ : PseudoEMetricSpace α
δ✝ ε : ℝ
s t : Set α
x : α
hst : Disjoint s t
hs : IsCompact s
ht : IsClosed t
δ : ℝ
hδ : 0 < δ
h : Disjoint (thickening δ s) (thickening δ t)
⊢ cthickening (δ / 2) t ≤ thickening δ t
[PROOFSTEP]
exact cthickening_subset_thickening' hδ (half_lt_self hδ) _
[GOAL]
ι : Sort u_1
α : Type u
β : Type v
inst✝¹ : PseudoEMetricSpace α
δ ε : ℝ
s t : Set α
x : α
inst✝ : LocallyCompactSpace α
hs : IsCompact s
⊢ ∃ δ, 0 < δ ∧ IsCompact (cthickening δ s)
[PROOFSTEP]
rcases exists_compact_superset hs with ⟨K, K_compact, hK⟩
[GOAL]
case intro.intro
ι : Sort u_1
α : Type u
β : Type v
inst✝¹ : PseudoEMetricSpace α
δ ε : ℝ
s t : Set α
x : α
inst✝ : LocallyCompactSpace α
hs : IsCompact s
K : Set α
K_compact : IsCompact K
hK : s ⊆ interior K
⊢ ∃ δ, 0 < δ ∧ IsCompact (cthickening δ s)
[PROOFSTEP]
rcases hs.exists_cthickening_subset_open isOpen_interior hK with ⟨δ, δpos, hδ⟩
[GOAL]
case intro.intro.intro.intro
ι : Sort u_1
α : Type u
β : Type v
inst✝¹ : PseudoEMetricSpace α
δ✝ ε : ℝ
s t : Set α
x : α
inst✝ : LocallyCompactSpace α
hs : IsCompact s
K : Set α
K_compact : IsCompact K
hK : s ⊆ interior K
δ : ℝ
δpos : 0 < δ
hδ : cthickening δ s ⊆ interior K
⊢ ∃ δ, 0 < δ ∧ IsCompact (cthickening δ s)
[PROOFSTEP]
refine ⟨δ, δpos, ?_⟩
[GOAL]
case intro.intro.intro.intro
ι : Sort u_1
α : Type u
β : Type v
inst✝¹ : PseudoEMetricSpace α
δ✝ ε : ℝ
s t : Set α
x : α
inst✝ : LocallyCompactSpace α
hs : IsCompact s
K : Set α
K_compact : IsCompact K
hK : s ⊆ interior K
δ : ℝ
δpos : 0 < δ
hδ : cthickening δ s ⊆ interior K
⊢ IsCompact (cthickening δ s)
[PROOFSTEP]
exact isCompact_of_isClosed_subset K_compact isClosed_cthickening (hδ.trans interior_subset)
[GOAL]
ι : Sort u_1
α : Type u
β : Type v
inst✝ : PseudoEMetricSpace α
δ✝ ε : ℝ
s✝ t : Set α
x : α
δ : ℝ
s : Set ℝ
hsδ : s ⊆ Ioi δ
hs : ∀ (ε : ℝ), δ < ε → Set.Nonempty (s ∩ Ioc δ ε)
E : Set α
⊢ cthickening δ E = ⋂ (ε : ℝ) (_ : ε ∈ s), cthickening ε E
[PROOFSTEP]
apply Subset.antisymm
[GOAL]
case h₁
ι : Sort u_1
α : Type u
β : Type v
inst✝ : PseudoEMetricSpace α
δ✝ ε : ℝ
s✝ t : Set α
x : α
δ : ℝ
s : Set ℝ
hsδ : s ⊆ Ioi δ
hs : ∀ (ε : ℝ), δ < ε → Set.Nonempty (s ∩ Ioc δ ε)
E : Set α
⊢ cthickening δ E ⊆ ⋂ (ε : ℝ) (_ : ε ∈ s), cthickening ε E
[PROOFSTEP]
exact subset_iInter₂ fun _ hε => cthickening_mono (le_of_lt (hsδ hε)) E
[GOAL]
case h₂
ι : Sort u_1
α : Type u
β : Type v
inst✝ : PseudoEMetricSpace α
δ✝ ε : ℝ
s✝ t : Set α
x : α
δ : ℝ
s : Set ℝ
hsδ : s ⊆ Ioi δ
hs : ∀ (ε : ℝ), δ < ε → Set.Nonempty (s ∩ Ioc δ ε)
E : Set α
⊢ ⋂ (ε : ℝ) (_ : ε ∈ s), cthickening ε E ⊆ cthickening δ E
[PROOFSTEP]
unfold cthickening
[GOAL]
case h₂
ι : Sort u_1
α : Type u
β : Type v
inst✝ : PseudoEMetricSpace α
δ✝ ε : ℝ
s✝ t : Set α
x : α
δ : ℝ
s : Set ℝ
hsδ : s ⊆ Ioi δ
hs : ∀ (ε : ℝ), δ < ε → Set.Nonempty (s ∩ Ioc δ ε)
E : Set α
⊢ ⋂ (ε : ℝ) (_ : ε ∈ s), {x | infEdist x E ≤ ENNReal.ofReal ε} ⊆ {x | infEdist x E ≤ ENNReal.ofReal δ}
[PROOFSTEP]
intro x hx
[GOAL]
case h₂
ι : Sort u_1
α : Type u
β : Type v
inst✝ : PseudoEMetricSpace α
δ✝ ε : ℝ
s✝ t : Set α
x✝ : α
δ : ℝ
s : Set ℝ
hsδ : s ⊆ Ioi δ
hs : ∀ (ε : ℝ), δ < ε → Set.Nonempty (s ∩ Ioc δ ε)
E : Set α
x : α
hx : x ∈ ⋂ (ε : ℝ) (_ : ε ∈ s), {x | infEdist x E ≤ ENNReal.ofReal ε}
⊢ x ∈ {x | infEdist x E ≤ ENNReal.ofReal δ}
[PROOFSTEP]
simp only [mem_iInter, mem_setOf_eq] at *
[GOAL]
case h₂
ι : Sort u_1
α : Type u
β : Type v
inst✝ : PseudoEMetricSpace α
δ✝ ε : ℝ
s✝ t : Set α
x✝ : α
δ : ℝ
s : Set ℝ
hsδ : s ⊆ Ioi δ
hs : ∀ (ε : ℝ), δ < ε → Set.Nonempty (s ∩ Ioc δ ε)
E : Set α
x : α
hx : ∀ (i : ℝ), i ∈ s → infEdist x E ≤ ENNReal.ofReal i
⊢ infEdist x E ≤ ENNReal.ofReal δ
[PROOFSTEP]
apply ENNReal.le_of_forall_pos_le_add
[GOAL]
case h₂.h
ι : Sort u_1
α : Type u
β : Type v
inst✝ : PseudoEMetricSpace α
δ✝ ε : ℝ
s✝ t : Set α
x✝ : α
δ : ℝ
s : Set ℝ
hsδ : s ⊆ Ioi δ
hs : ∀ (ε : ℝ), δ < ε → Set.Nonempty (s ∩ Ioc δ ε)
E : Set α
x : α
hx : ∀ (i : ℝ), i ∈ s → infEdist x E ≤ ENNReal.ofReal i
⊢ ∀ (ε : ℝ≥0), 0 < ε → ENNReal.ofReal δ < ⊤ → infEdist x E ≤ ENNReal.ofReal δ + ↑ε
[PROOFSTEP]
intro η η_pos _
[GOAL]
case h₂.h
ι : Sort u_1
α : Type u
β : Type v
inst✝ : PseudoEMetricSpace α
δ✝ ε : ℝ
s✝ t : Set α
x✝ : α
δ : ℝ
s : Set ℝ
hsδ : s ⊆ Ioi δ
hs : ∀ (ε : ℝ), δ < ε → Set.Nonempty (s ∩ Ioc δ ε)
E : Set α
x : α
hx : ∀ (i : ℝ), i ∈ s → infEdist x E ≤ ENNReal.ofReal i
η : ℝ≥0
η_pos : 0 < η
a✝ : ENNReal.ofReal δ < ⊤
⊢ infEdist x E ≤ ENNReal.ofReal δ + ↑η
[PROOFSTEP]
rcases hs (δ + η) (lt_add_of_pos_right _ (NNReal.coe_pos.mpr η_pos)) with ⟨ε, ⟨hsε, hε⟩⟩
[GOAL]
case h₂.h.intro.intro
ι : Sort u_1
α : Type u
β : Type v
inst✝ : PseudoEMetricSpace α
δ✝ ε✝ : ℝ
s✝ t : Set α
x✝ : α
δ : ℝ
s : Set ℝ
hsδ : s ⊆ Ioi δ
hs : ∀ (ε : ℝ), δ < ε → Set.Nonempty (s ∩ Ioc δ ε)
E : Set α
x : α
hx : ∀ (i : ℝ), i ∈ s → infEdist x E ≤ ENNReal.ofReal i
η : ℝ≥0
η_pos : 0 < η
a✝ : ENNReal.ofReal δ < ⊤
ε : ℝ
hsε : ε ∈ s
hε : ε ∈ Ioc δ (δ + ↑η)
⊢ infEdist x E ≤ ENNReal.ofReal δ + ↑η
[PROOFSTEP]
apply ((hx ε hsε).trans (ENNReal.ofReal_le_ofReal hε.2)).trans
[GOAL]
case h₂.h.intro.intro
ι : Sort u_1
α : Type u
β : Type v
inst✝ : PseudoEMetricSpace α
δ✝ ε✝ : ℝ
s✝ t : Set α
x✝ : α
δ : ℝ
s : Set ℝ
hsδ : s ⊆ Ioi δ
hs : ∀ (ε : ℝ), δ < ε → Set.Nonempty (s ∩ Ioc δ ε)
E : Set α
x : α
hx : ∀ (i : ℝ), i ∈ s → infEdist x E ≤ ENNReal.ofReal i
η : ℝ≥0
η_pos : 0 < η
a✝ : ENNReal.ofReal δ < ⊤
ε : ℝ
hsε : ε ∈ s
hε : ε ∈ Ioc δ (δ + ↑η)
⊢ ENNReal.ofReal (δ + ↑η) ≤ ENNReal.ofReal δ + ↑η
[PROOFSTEP]
rw [ENNReal.coe_nnreal_eq η]
[GOAL]
case h₂.h.intro.intro
ι : Sort u_1
α : Type u
β : Type v
inst✝ : PseudoEMetricSpace α
δ✝ ε✝ : ℝ
s✝ t : Set α
x✝ : α
δ : ℝ
s : Set ℝ
hsδ : s ⊆ Ioi δ
hs : ∀ (ε : ℝ), δ < ε → Set.Nonempty (s ∩ Ioc δ ε)
E : Set α
x : α
hx : ∀ (i : ℝ), i ∈ s → infEdist x E ≤ ENNReal.ofReal i
η : ℝ≥0
η_pos : 0 < η
a✝ : ENNReal.ofReal δ < ⊤
ε : ℝ
hsε : ε ∈ s
hε : ε ∈ Ioc δ (δ + ↑η)
⊢ ENNReal.ofReal (δ + ↑η) ≤ ENNReal.ofReal δ + ENNReal.ofReal ↑η
[PROOFSTEP]
exact ENNReal.ofReal_add_le
[GOAL]
ι : Sort u_1
α : Type u
β : Type v
inst✝ : PseudoEMetricSpace α
δ✝ ε : ℝ
s t : Set α
x : α
δ : ℝ
E : Set α
⊢ cthickening δ E = ⋂ (ε : ℝ) (_ : δ < ε), cthickening ε E
[PROOFSTEP]
apply cthickening_eq_iInter_cthickening' (Ioi δ) rfl.subset
[GOAL]
case hs
ι : Sort u_1
α : Type u
β : Type v
inst✝ : PseudoEMetricSpace α
δ✝ ε : ℝ
s t : Set α
x : α
δ : ℝ
E : Set α
⊢ ∀ (ε : ℝ), δ < ε → Set.Nonempty (Ioi δ ∩ Ioc δ ε)
[PROOFSTEP]
simp_rw [inter_eq_right_iff_subset.mpr Ioc_subset_Ioi_self]
[GOAL]
case hs
ι : Sort u_1
α : Type u
β : Type v
inst✝ : PseudoEMetricSpace α
δ✝ ε : ℝ
s t : Set α
x : α
δ : ℝ
E : Set α
⊢ ∀ (ε : ℝ), δ < ε → Set.Nonempty (Ioc δ ε)
[PROOFSTEP]
exact fun _ hε => nonempty_Ioc.mpr hε
[GOAL]
ι : Sort u_1
α : Type u
β : Type v
inst✝ : PseudoEMetricSpace α
δ✝ ε : ℝ
s✝ t : Set α
x : α
δ : ℝ
δ_nn : 0 ≤ δ
s : Set ℝ
hsδ : s ⊆ Ioi δ
hs : ∀ (ε : ℝ), δ < ε → Set.Nonempty (s ∩ Ioc δ ε)
E : Set α
⊢ cthickening δ E = ⋂ (ε : ℝ) (_ : ε ∈ s), thickening ε E
[PROOFSTEP]
refine' (subset_iInter₂ fun ε hε => _).antisymm _
[GOAL]
case refine'_1
ι : Sort u_1
α : Type u
β : Type v
inst✝ : PseudoEMetricSpace α
δ✝ ε✝ : ℝ
s✝ t : Set α
x : α
δ : ℝ
δ_nn : 0 ≤ δ
s : Set ℝ
hsδ : s ⊆ Ioi δ
hs : ∀ (ε : ℝ), δ < ε → Set.Nonempty (s ∩ Ioc δ ε)
E : Set α
ε : ℝ
hε : ε ∈ s
⊢ cthickening δ E ⊆ thickening ε E
[PROOFSTEP]
obtain ⟨ε', -, hε'⟩ := hs ε (hsδ hε)
[GOAL]
case refine'_1.intro.intro
ι : Sort u_1
α : Type u
β : Type v
inst✝ : PseudoEMetricSpace α
δ✝ ε✝ : ℝ
s✝ t : Set α
x : α
δ : ℝ
δ_nn : 0 ≤ δ
s : Set ℝ
hsδ : s ⊆ Ioi δ
hs : ∀ (ε : ℝ), δ < ε → Set.Nonempty (s ∩ Ioc δ ε)
E : Set α
ε : ℝ
hε : ε ∈ s
ε' : ℝ
hε' : ε' ∈ Ioc δ ε
⊢ cthickening δ E ⊆ thickening ε E
[PROOFSTEP]
have ss := cthickening_subset_thickening' (lt_of_le_of_lt δ_nn hε'.1) hε'.1 E
[GOAL]
case refine'_1.intro.intro
ι : Sort u_1
α : Type u
β : Type v
inst✝ : PseudoEMetricSpace α
δ✝ ε✝ : ℝ
s✝ t : Set α
x : α
δ : ℝ
δ_nn : 0 ≤ δ
s : Set ℝ
hsδ : s ⊆ Ioi δ
hs : ∀ (ε : ℝ), δ < ε → Set.Nonempty (s ∩ Ioc δ ε)
E : Set α
ε : ℝ
hε : ε ∈ s
ε' : ℝ
hε' : ε' ∈ Ioc δ ε
ss : cthickening δ E ⊆ thickening ε' E
⊢ cthickening δ E ⊆ thickening ε E
[PROOFSTEP]
exact ss.trans (thickening_mono hε'.2 E)
[GOAL]
case refine'_2
ι : Sort u_1
α : Type u
β : Type v
inst✝ : PseudoEMetricSpace α
δ✝ ε : ℝ
s✝ t : Set α
x : α
δ : ℝ
δ_nn : 0 ≤ δ
s : Set ℝ
hsδ : s ⊆ Ioi δ
hs : ∀ (ε : ℝ), δ < ε → Set.Nonempty (s ∩ Ioc δ ε)
E : Set α
⊢ ⋂ (i : ℝ) (_ : i ∈ s), thickening i E ⊆ cthickening δ E
[PROOFSTEP]
rw [cthickening_eq_iInter_cthickening' s hsδ hs E]
[GOAL]
case refine'_2
ι : Sort u_1
α : Type u
β : Type v
inst✝ : PseudoEMetricSpace α
δ✝ ε : ℝ
s✝ t : Set α
x : α
δ : ℝ
δ_nn : 0 ≤ δ
s : Set ℝ
hsδ : s ⊆ Ioi δ
hs : ∀ (ε : ℝ), δ < ε → Set.Nonempty (s ∩ Ioc δ ε)
E : Set α
⊢ ⋂ (i : ℝ) (_ : i ∈ s), thickening i E ⊆ ⋂ (ε : ℝ) (_ : ε ∈ s), cthickening ε E
[PROOFSTEP]
exact iInter₂_mono fun ε _ => thickening_subset_cthickening ε E
[GOAL]
ι : Sort u_1
α : Type u
β : Type v
inst✝ : PseudoEMetricSpace α
δ✝ ε : ℝ
s t : Set α
x : α
δ : ℝ
δ_nn : 0 ≤ δ
E : Set α
⊢ cthickening δ E = ⋂ (ε : ℝ) (_ : δ < ε), thickening ε E
[PROOFSTEP]
apply cthickening_eq_iInter_thickening' δ_nn (Ioi δ) rfl.subset
[GOAL]
case hs
ι : Sort u_1
α : Type u
β : Type v
inst✝ : PseudoEMetricSpace α
δ✝ ε : ℝ
s t : Set α
x : α
δ : ℝ
δ_nn : 0 ≤ δ
E : Set α
⊢ ∀ (ε : ℝ), δ < ε → Set.Nonempty (Ioi δ ∩ Ioc δ ε)
[PROOFSTEP]
simp_rw [inter_eq_right_iff_subset.mpr Ioc_subset_Ioi_self]
[GOAL]
case hs
ι : Sort u_1
α : Type u
β : Type v
inst✝ : PseudoEMetricSpace α
δ✝ ε : ℝ
s t : Set α
x : α
δ : ℝ
δ_nn : 0 ≤ δ
E : Set α
⊢ ∀ (ε : ℝ), δ < ε → Set.Nonempty (Ioc δ ε)
[PROOFSTEP]
exact fun _ hε => nonempty_Ioc.mpr hε
[GOAL]
ι : Sort u_1
α : Type u
β : Type v
inst✝ : PseudoEMetricSpace α
δ✝ ε : ℝ
s t : Set α
x : α
δ : ℝ
E : Set α
⊢ cthickening δ E = ⋂ (ε : ℝ) (_ : max 0 δ < ε), thickening ε E
[PROOFSTEP]
rw [← cthickening_max_zero, cthickening_eq_iInter_thickening]
[GOAL]
case δ_nn
ι : Sort u_1
α : Type u
β : Type v
inst✝ : PseudoEMetricSpace α
δ✝ ε : ℝ
s t : Set α
x : α
δ : ℝ
E : Set α
⊢ 0 ≤ max 0 δ
[PROOFSTEP]
exact le_max_left _ _
[GOAL]
ι : Sort u_1
α : Type u
β : Type v
inst✝ : PseudoEMetricSpace α
δ ε : ℝ
s✝ t : Set α
x : α
E : Set α
s : Set ℝ
hs : ∀ (ε : ℝ), 0 < ε → Set.Nonempty (s ∩ Ioc 0 ε)
⊢ closure E = ⋂ (δ : ℝ) (_ : δ ∈ s), cthickening δ E
[PROOFSTEP]
by_cases hs₀ : s ⊆ Ioi 0
[GOAL]
case pos
ι : Sort u_1
α : Type u
β : Type v
inst✝ : PseudoEMetricSpace α
δ ε : ℝ
s✝ t : Set α
x : α
E : Set α
s : Set ℝ
hs : ∀ (ε : ℝ), 0 < ε → Set.Nonempty (s ∩ Ioc 0 ε)
hs₀ : s ⊆ Ioi 0
⊢ closure E = ⋂ (δ : ℝ) (_ : δ ∈ s), cthickening δ E
[PROOFSTEP]
rw [← cthickening_zero]
[GOAL]
case pos
ι : Sort u_1
α : Type u
β : Type v
inst✝ : PseudoEMetricSpace α
δ ε : ℝ
s✝ t : Set α
x : α
E : Set α
s : Set ℝ
hs : ∀ (ε : ℝ), 0 < ε → Set.Nonempty (s ∩ Ioc 0 ε)
hs₀ : s ⊆ Ioi 0
⊢ cthickening 0 E = ⋂ (δ : ℝ) (_ : δ ∈ s), cthickening δ E
[PROOFSTEP]
apply cthickening_eq_iInter_cthickening' _ hs₀ hs
[GOAL]
case neg
ι : Sort u_1
α : Type u
β : Type v
inst✝ : PseudoEMetricSpace α
δ ε : ℝ
s✝ t : Set α
x : α
E : Set α
s : Set ℝ
hs : ∀ (ε : ℝ), 0 < ε → Set.Nonempty (s ∩ Ioc 0 ε)
hs₀ : ¬s ⊆ Ioi 0
⊢ closure E = ⋂ (δ : ℝ) (_ : δ ∈ s), cthickening δ E
[PROOFSTEP]
obtain ⟨δ, hδs, δ_nonpos⟩ := not_subset.mp hs₀
[GOAL]
case neg.intro.intro
ι : Sort u_1
α : Type u
β : Type v
inst✝ : PseudoEMetricSpace α
δ✝ ε : ℝ
s✝ t : Set α
x : α
E : Set α
s : Set ℝ
hs : ∀ (ε : ℝ), 0 < ε → Set.Nonempty (s ∩ Ioc 0 ε)
hs₀ : ¬s ⊆ Ioi 0
δ : ℝ
hδs : δ ∈ s
δ_nonpos : ¬δ ∈ Ioi 0
⊢ closure E = ⋂ (δ : ℝ) (_ : δ ∈ s), cthickening δ E
[PROOFSTEP]
rw [Set.mem_Ioi, not_lt] at δ_nonpos 
[GOAL]
case neg.intro.intro
ι : Sort u_1
α : Type u
β : Type v
inst✝ : PseudoEMetricSpace α
δ✝ ε : ℝ
s✝ t : Set α
x : α
E : Set α
s : Set ℝ
hs : ∀ (ε : ℝ), 0 < ε → Set.Nonempty (s ∩ Ioc 0 ε)
hs₀ : ¬s ⊆ Ioi 0
δ : ℝ
hδs : δ ∈ s
δ_nonpos : δ ≤ 0
⊢ closure E = ⋂ (δ : ℝ) (_ : δ ∈ s), cthickening δ E
[PROOFSTEP]
apply Subset.antisymm
[GOAL]
case neg.intro.intro.h₁
ι : Sort u_1
α : Type u
β : Type v
inst✝ : PseudoEMetricSpace α
δ✝ ε : ℝ
s✝ t : Set α
x : α
E : Set α
s : Set ℝ
hs : ∀ (ε : ℝ), 0 < ε → Set.Nonempty (s ∩ Ioc 0 ε)
hs₀ : ¬s ⊆ Ioi 0
δ : ℝ
hδs : δ ∈ s
δ_nonpos : δ ≤ 0
⊢ closure E ⊆ ⋂ (δ : ℝ) (_ : δ ∈ s), cthickening δ E
[PROOFSTEP]
exact subset_iInter₂ fun ε _ => closure_subset_cthickening ε E
[GOAL]
case neg.intro.intro.h₂
ι : Sort u_1
α : Type u
β : Type v
inst✝ : PseudoEMetricSpace α
δ✝ ε : ℝ
s✝ t : Set α
x : α
E : Set α
s : Set ℝ
hs : ∀ (ε : ℝ), 0 < ε → Set.Nonempty (s ∩ Ioc 0 ε)
hs₀ : ¬s ⊆ Ioi 0
δ : ℝ
hδs : δ ∈ s
δ_nonpos : δ ≤ 0
⊢ ⋂ (δ : ℝ) (_ : δ ∈ s), cthickening δ E ⊆ closure E
[PROOFSTEP]
rw [← cthickening_of_nonpos δ_nonpos E]
[GOAL]
case neg.intro.intro.h₂
ι : Sort u_1
α : Type u
β : Type v
inst✝ : PseudoEMetricSpace α
δ✝ ε : ℝ
s✝ t : Set α
x : α
E : Set α
s : Set ℝ
hs : ∀ (ε : ℝ), 0 < ε → Set.Nonempty (s ∩ Ioc 0 ε)
hs₀ : ¬s ⊆ Ioi 0
δ : ℝ
hδs : δ ∈ s
δ_nonpos : δ ≤ 0
⊢ ⋂ (δ : ℝ) (_ : δ ∈ s), cthickening δ E ⊆ cthickening δ E
[PROOFSTEP]
exact biInter_subset_of_mem hδs
[GOAL]
ι : Sort u_1
α : Type u
β : Type v
inst✝ : PseudoEMetricSpace α
δ ε : ℝ
s t : Set α
x : α
E : Set α
⊢ closure E = ⋂ (δ : ℝ) (_ : 0 < δ), cthickening δ E
[PROOFSTEP]
rw [← cthickening_zero]
[GOAL]
ι : Sort u_1
α : Type u
β : Type v
inst✝ : PseudoEMetricSpace α
δ ε : ℝ
s t : Set α
x : α
E : Set α
⊢ cthickening 0 E = ⋂ (δ : ℝ) (_ : 0 < δ), cthickening δ E
[PROOFSTEP]
exact cthickening_eq_iInter_cthickening E
[GOAL]
ι : Sort u_1
α : Type u
β : Type v
inst✝ : PseudoEMetricSpace α
δ ε : ℝ
s✝ t : Set α
x : α
E : Set α
s : Set ℝ
hs₀ : s ⊆ Ioi 0
hs : ∀ (ε : ℝ), 0 < ε → Set.Nonempty (s ∩ Ioc 0 ε)
⊢ closure E = ⋂ (δ : ℝ) (_ : δ ∈ s), thickening δ E
[PROOFSTEP]
rw [← cthickening_zero]
[GOAL]
ι : Sort u_1
α : Type u
β : Type v
inst✝ : PseudoEMetricSpace α
δ ε : ℝ
s✝ t : Set α
x : α
E : Set α
s : Set ℝ
hs₀ : s ⊆ Ioi 0
hs : ∀ (ε : ℝ), 0 < ε → Set.Nonempty (s ∩ Ioc 0 ε)
⊢ cthickening 0 E = ⋂ (δ : ℝ) (_ : δ ∈ s), thickening δ E
[PROOFSTEP]
apply cthickening_eq_iInter_thickening' le_rfl _ hs₀ hs
[GOAL]
ι : Sort u_1
α : Type u
β : Type v
inst✝ : PseudoEMetricSpace α
δ ε : ℝ
s t : Set α
x : α
E : Set α
⊢ closure E = ⋂ (δ : ℝ) (_ : 0 < δ), thickening δ E
[PROOFSTEP]
rw [← cthickening_zero]
[GOAL]
ι : Sort u_1
α : Type u
β : Type v
inst✝ : PseudoEMetricSpace α
δ ε : ℝ
s t : Set α
x : α
E : Set α
⊢ cthickening 0 E = ⋂ (δ : ℝ) (_ : 0 < δ), thickening δ E
[PROOFSTEP]
exact cthickening_eq_iInter_thickening rfl.ge E
[GOAL]
ι : Sort u_1
α✝ : Type u
β : Type v
inst✝¹ : PseudoEMetricSpace α✝
δ✝ ε : ℝ
s t : Set α✝
x✝ : α✝
α : Type u_2
inst✝ : PseudoMetricSpace α
x : α
E : Set α
hx : x ∈ E
δ : ℝ
⊢ closedBall x δ ⊆ cthickening δ E
[PROOFSTEP]
refine' (closedBall_subset_cthickening_singleton _ _).trans (cthickening_subset_of_subset _ _)
[GOAL]
ι : Sort u_1
α✝ : Type u
β : Type v
inst✝¹ : PseudoEMetricSpace α✝
δ✝ ε : ℝ
s t : Set α✝
x✝ : α✝
α : Type u_2
inst✝ : PseudoMetricSpace α
x : α
E : Set α
hx : x ∈ E
δ : ℝ
⊢ {x} ⊆ E
[PROOFSTEP]
simpa using hx
[GOAL]
ι : Sort u_1
α✝ : Type u
β : Type v
inst✝¹ : PseudoEMetricSpace α✝
δ✝ ε : ℝ
s t : Set α✝
x : α✝
α : Type u_2
inst✝ : PseudoMetricSpace α
E : Set α
δ δ' : ℝ
hδ₀ : 0 < δ'
hδδ' : δ < δ'
⊢ cthickening δ E ⊆ ⋃ (x : α) (_ : x ∈ E), closedBall x δ'
[PROOFSTEP]
refine' (cthickening_subset_thickening' hδ₀ hδδ' E).trans fun x hx => _
[GOAL]
ι : Sort u_1
α✝ : Type u
β : Type v
inst✝¹ : PseudoEMetricSpace α✝
δ✝ ε : ℝ
s t : Set α✝
x✝ : α✝
α : Type u_2
inst✝ : PseudoMetricSpace α
E : Set α
δ δ' : ℝ
hδ₀ : 0 < δ'
hδδ' : δ < δ'
x : α
hx : x ∈ thickening δ' E
⊢ x ∈ ⋃ (x : α) (_ : x ∈ E), closedBall x δ'
[PROOFSTEP]
obtain ⟨y, hy₁, hy₂⟩ := mem_thickening_iff.mp hx
[GOAL]
case intro.intro
ι : Sort u_1
α✝ : Type u
β : Type v
inst✝¹ : PseudoEMetricSpace α✝
δ✝ ε : ℝ
s t : Set α✝
x✝ : α✝
α : Type u_2
inst✝ : PseudoMetricSpace α
E : Set α
δ δ' : ℝ
hδ₀ : 0 < δ'
hδδ' : δ < δ'
x : α
hx : x ∈ thickening δ' E
y : α
hy₁ : y ∈ E
hy₂ : dist x y < δ'
⊢ x ∈ ⋃ (x : α) (_ : x ∈ E), closedBall x δ'
[PROOFSTEP]
exact mem_iUnion₂.mpr ⟨y, hy₁, hy₂.le⟩
[GOAL]
ι : Sort u_1
α✝ : Type u
β : Type v
inst✝¹ : PseudoEMetricSpace α✝
δ✝ ε : ℝ
s t : Set α✝
x : α✝
α : Type u_2
inst✝ : PseudoMetricSpace α
δ : ℝ
E : Set α
hE : IsCompact E
hδ : 0 ≤ δ
⊢ cthickening δ E = ⋃ (x : α) (_ : x ∈ E), closedBall x δ
[PROOFSTEP]
rcases eq_empty_or_nonempty E with (rfl | hne)
[GOAL]
case inl
ι : Sort u_1
α✝ : Type u
β : Type v
inst✝¹ : PseudoEMetricSpace α✝
δ✝ ε : ℝ
s t : Set α✝
x : α✝
α : Type u_2
inst✝ : PseudoMetricSpace α
δ : ℝ
hδ : 0 ≤ δ
hE : IsCompact ∅
⊢ cthickening δ ∅ = ⋃ (x : α) (_ : x ∈ ∅), closedBall x δ
[PROOFSTEP]
simp only [cthickening_empty, biUnion_empty]
[GOAL]
case inr
ι : Sort u_1
α✝ : Type u
β : Type v
inst✝¹ : PseudoEMetricSpace α✝
δ✝ ε : ℝ
s t : Set α✝
x : α✝
α : Type u_2
inst✝ : PseudoMetricSpace α
δ : ℝ
E : Set α
hE : IsCompact E
hδ : 0 ≤ δ
hne : Set.Nonempty E
⊢ cthickening δ E = ⋃ (x : α) (_ : x ∈ E), closedBall x δ
[PROOFSTEP]
refine Subset.antisymm (fun x hx ↦ ?_) (iUnion₂_subset fun x hx ↦ closedBall_subset_cthickening hx _)
[GOAL]
case inr
ι : Sort u_1
α✝ : Type u
β : Type v
inst✝¹ : PseudoEMetricSpace α✝
δ✝ ε : ℝ
s t : Set α✝
x✝ : α✝
α : Type u_2
inst✝ : PseudoMetricSpace α
δ : ℝ
E : Set α
hE : IsCompact E
hδ : 0 ≤ δ
hne : Set.Nonempty E
x : α
hx : x ∈ cthickening δ E
⊢ x ∈ ⋃ (x : α) (_ : x ∈ E), closedBall x δ
[PROOFSTEP]
obtain ⟨y, yE, hy⟩ : ∃ y ∈ E, infEdist x E = edist x y := hE.exists_infEdist_eq_edist hne _
[GOAL]
case inr.intro.intro
ι : Sort u_1
α✝ : Type u
β : Type v
inst✝¹ : PseudoEMetricSpace α✝
δ✝ ε : ℝ
s t : Set α✝
x✝ : α✝
α : Type u_2
inst✝ : PseudoMetricSpace α
δ : ℝ
E : Set α
hE : IsCompact E
hδ : 0 ≤ δ
hne : Set.Nonempty E
x : α
hx : x ∈ cthickening δ E
y : α
yE : y ∈ E
hy : infEdist x E = edist x y
⊢ x ∈ ⋃ (x : α) (_ : x ∈ E), closedBall x δ
[PROOFSTEP]
have D1 : edist x y ≤ ENNReal.ofReal δ := (le_of_eq hy.symm).trans hx
[GOAL]
case inr.intro.intro
ι : Sort u_1
α✝ : Type u
β : Type v
inst✝¹ : PseudoEMetricSpace α✝
δ✝ ε : ℝ
s t : Set α✝
x✝ : α✝
α : Type u_2
inst✝ : PseudoMetricSpace α
δ : ℝ
E : Set α
hE : IsCompact E
hδ : 0 ≤ δ
hne : Set.Nonempty E
x : α
hx : x ∈ cthickening δ E
y : α
yE : y ∈ E
hy : infEdist x E = edist x y
D1 : edist x y ≤ ENNReal.ofReal δ
⊢ x ∈ ⋃ (x : α) (_ : x ∈ E), closedBall x δ
[PROOFSTEP]
have D2 : dist x y ≤ δ := by
  rw [edist_dist] at D1 
  exact (ENNReal.ofReal_le_ofReal_iff hδ).1 D1
[GOAL]
ι : Sort u_1
α✝ : Type u
β : Type v
inst✝¹ : PseudoEMetricSpace α✝
δ✝ ε : ℝ
s t : Set α✝
x✝ : α✝
α : Type u_2
inst✝ : PseudoMetricSpace α
δ : ℝ
E : Set α
hE : IsCompact E
hδ : 0 ≤ δ
hne : Set.Nonempty E
x : α
hx : x ∈ cthickening δ E
y : α
yE : y ∈ E
hy : infEdist x E = edist x y
D1 : edist x y ≤ ENNReal.ofReal δ
⊢ dist x y ≤ δ
[PROOFSTEP]
rw [edist_dist] at D1 
[GOAL]
ι : Sort u_1
α✝ : Type u
β : Type v
inst✝¹ : PseudoEMetricSpace α✝
δ✝ ε : ℝ
s t : Set α✝
x✝ : α✝
α : Type u_2
inst✝ : PseudoMetricSpace α
δ : ℝ
E : Set α
hE : IsCompact E
hδ : 0 ≤ δ
hne : Set.Nonempty E
x : α
hx : x ∈ cthickening δ E
y : α
yE : y ∈ E
hy : infEdist x E = edist x y
D1 : ENNReal.ofReal (dist x y) ≤ ENNReal.ofReal δ
⊢ dist x y ≤ δ
[PROOFSTEP]
exact (ENNReal.ofReal_le_ofReal_iff hδ).1 D1
[GOAL]
case inr.intro.intro
ι : Sort u_1
α✝ : Type u
β : Type v
inst✝¹ : PseudoEMetricSpace α✝
δ✝ ε : ℝ
s t : Set α✝
x✝ : α✝
α : Type u_2
inst✝ : PseudoMetricSpace α
δ : ℝ
E : Set α
hE : IsCompact E
hδ : 0 ≤ δ
hne : Set.Nonempty E
x : α
hx : x ∈ cthickening δ E
y : α
yE : y ∈ E
hy : infEdist x E = edist x y
D1 : edist x y ≤ ENNReal.ofReal δ
D2 : dist x y ≤ δ
⊢ x ∈ ⋃ (x : α) (_ : x ∈ E), closedBall x δ
[PROOFSTEP]
exact mem_biUnion yE D2
[GOAL]
ι : Sort u_1
α✝ : Type u
β : Type v
inst✝² : PseudoEMetricSpace α✝
δ ε : ℝ
s t : Set α✝
x : α✝
α : Type u_2
inst✝¹ : PseudoMetricSpace α
inst✝ : ProperSpace α
E : Set α
hδ : 0 ≤ δ
⊢ cthickening δ E = ⋃ (x : α) (_ : x ∈ closure E), closedBall x δ
[PROOFSTEP]
rcases eq_empty_or_nonempty E with (rfl | hne)
[GOAL]
case inl
ι : Sort u_1
α✝ : Type u
β : Type v
inst✝² : PseudoEMetricSpace α✝
δ ε : ℝ
s t : Set α✝
x : α✝
α : Type u_2
inst✝¹ : PseudoMetricSpace α
inst✝ : ProperSpace α
hδ : 0 ≤ δ
⊢ cthickening δ ∅ = ⋃ (x : α) (_ : x ∈ closure ∅), closedBall x δ
[PROOFSTEP]
simp only [cthickening_empty, biUnion_empty, closure_empty]
[GOAL]
case inr
ι : Sort u_1
α✝ : Type u
β : Type v
inst✝² : PseudoEMetricSpace α✝
δ ε : ℝ
s t : Set α✝
x : α✝
α : Type u_2
inst✝¹ : PseudoMetricSpace α
inst✝ : ProperSpace α
E : Set α
hδ : 0 ≤ δ
hne : Set.Nonempty E
⊢ cthickening δ E = ⋃ (x : α) (_ : x ∈ closure E), closedBall x δ
[PROOFSTEP]
rw [← cthickening_closure]
[GOAL]
case inr
ι : Sort u_1
α✝ : Type u
β : Type v
inst✝² : PseudoEMetricSpace α✝
δ ε : ℝ
s t : Set α✝
x : α✝
α : Type u_2
inst✝¹ : PseudoMetricSpace α
inst✝ : ProperSpace α
E : Set α
hδ : 0 ≤ δ
hne : Set.Nonempty E
⊢ cthickening δ (closure E) = ⋃ (x : α) (_ : x ∈ closure E), closedBall x δ
[PROOFSTEP]
refine Subset.antisymm (fun x hx ↦ ?_) (iUnion₂_subset fun x hx ↦ closedBall_subset_cthickening hx _)
[GOAL]
case inr
ι : Sort u_1
α✝ : Type u
β : Type v
inst✝² : PseudoEMetricSpace α✝
δ ε : ℝ
s t : Set α✝
x✝ : α✝
α : Type u_2
inst✝¹ : PseudoMetricSpace α
inst✝ : ProperSpace α
E : Set α
hδ : 0 ≤ δ
hne : Set.Nonempty E
x : α
hx : x ∈ cthickening δ (closure E)
⊢ x ∈ ⋃ (x : α) (_ : x ∈ closure E), closedBall x δ
[PROOFSTEP]
obtain ⟨y, yE, hy⟩ : ∃ y ∈ closure E, infDist x (closure E) = dist x y :=
  isClosed_closure.exists_infDist_eq_dist (closure_nonempty_iff.mpr hne) x
[GOAL]
case inr.intro.intro
ι : Sort u_1
α✝ : Type u
β : Type v
inst✝² : PseudoEMetricSpace α✝
δ ε : ℝ
s t : Set α✝
x✝ : α✝
α : Type u_2
inst✝¹ : PseudoMetricSpace α
inst✝ : ProperSpace α
E : Set α
hδ : 0 ≤ δ
hne : Set.Nonempty E
x : α
hx : x ∈ cthickening δ (closure E)
y : α
yE : y ∈ closure E
hy : infDist x (closure E) = dist x y
⊢ x ∈ ⋃ (x : α) (_ : x ∈ closure E), closedBall x δ
[PROOFSTEP]
replace hy : dist x y ≤ δ :=
  (ENNReal.ofReal_le_ofReal_iff hδ).mp (((congr_arg ENNReal.ofReal hy.symm).le.trans ENNReal.ofReal_toReal_le).trans hx)
[GOAL]
case inr.intro.intro
ι : Sort u_1
α✝ : Type u
β : Type v
inst✝² : PseudoEMetricSpace α✝
δ ε : ℝ
s t : Set α✝
x✝ : α✝
α : Type u_2
inst✝¹ : PseudoMetricSpace α
inst✝ : ProperSpace α
E : Set α
hδ : 0 ≤ δ
hne : Set.Nonempty E
x : α
hx : x ∈ cthickening δ (closure E)
y : α
yE : y ∈ closure E
hy : dist x y ≤ δ
⊢ x ∈ ⋃ (x : α) (_ : x ∈ closure E), closedBall x δ
[PROOFSTEP]
exact mem_biUnion yE hy
[GOAL]
ι : Sort u_1
α✝ : Type u
β : Type v
inst✝² : PseudoEMetricSpace α✝
δ ε : ℝ
s t : Set α✝
x : α✝
α : Type u_2
inst✝¹ : PseudoMetricSpace α
inst✝ : ProperSpace α
E : Set α
hE : IsClosed E
hδ : 0 ≤ δ
⊢ cthickening δ E = ⋃ (x : α) (_ : x ∈ E), closedBall x δ
[PROOFSTEP]
rw [cthickening_eq_biUnion_closedBall E hδ, hE.closure_eq]
[GOAL]
ι : Sort u_1
α : Type u
β : Type v
inst✝ : PseudoEMetricSpace α
δ ε : ℝ
s t : Set α
x : α
⊢ infEdist x s ≤ infEdist x (cthickening δ s) + ENNReal.ofReal δ
[PROOFSTEP]
refine' le_of_forall_lt' fun r h => _
[GOAL]
ι : Sort u_1
α : Type u
β : Type v
inst✝ : PseudoEMetricSpace α
δ ε : ℝ
s t : Set α
x : α
r : ℝ≥0∞
h : infEdist x (cthickening δ s) + ENNReal.ofReal δ < r
⊢ infEdist x s < r
[PROOFSTEP]
simp_rw [← lt_tsub_iff_right, infEdist_lt_iff, mem_cthickening_iff] at h 
[GOAL]
ι : Sort u_1
α : Type u
β : Type v
inst✝ : PseudoEMetricSpace α
δ ε : ℝ
s t : Set α
x : α
r : ℝ≥0∞
h : ∃ y, infEdist y s ≤ ENNReal.ofReal δ ∧ edist x y < r - ENNReal.ofReal δ
⊢ infEdist x s < r
[PROOFSTEP]
obtain ⟨y, hy, hxy⟩ := h
[GOAL]
case intro.intro
ι : Sort u_1
α : Type u
β : Type v
inst✝ : PseudoEMetricSpace α
δ ε : ℝ
s t : Set α
x : α
r : ℝ≥0∞
y : α
hy : infEdist y s ≤ ENNReal.ofReal δ
hxy : edist x y < r - ENNReal.ofReal δ
⊢ infEdist x s < r
[PROOFSTEP]
exact
  infEdist_le_edist_add_infEdist.trans_lt
    ((ENNReal.add_lt_add_of_lt_of_le (hy.trans_lt ENNReal.ofReal_lt_top).ne hxy hy).trans_eq
      (tsub_add_cancel_of_le <| le_self_add.trans (lt_tsub_iff_left.1 hxy).le))
[GOAL]
ι : Sort u_1
α : Type u
β : Type v
inst✝ : PseudoEMetricSpace α
δ✝ ε✝ : ℝ
s✝ t : Set α
x : α
ε δ : ℝ
s : Set α
⊢ thickening ε (thickening δ s) ⊆ thickening (ε + δ) s
[PROOFSTEP]
obtain hε | hε := le_total ε 0
[GOAL]
case inl
ι : Sort u_1
α : Type u
β : Type v
inst✝ : PseudoEMetricSpace α
δ✝ ε✝ : ℝ
s✝ t : Set α
x : α
ε δ : ℝ
s : Set α
hε : ε ≤ 0
⊢ thickening ε (thickening δ s) ⊆ thickening (ε + δ) s
[PROOFSTEP]
simp only [thickening_of_nonpos hε, empty_subset]
[GOAL]
case inr
ι : Sort u_1
α : Type u
β : Type v
inst✝ : PseudoEMetricSpace α
δ✝ ε✝ : ℝ
s✝ t : Set α
x : α
ε δ : ℝ
s : Set α
hε : 0 ≤ ε
⊢ thickening ε (thickening δ s) ⊆ thickening (ε + δ) s
[PROOFSTEP]
obtain hδ | hδ := le_total δ 0
[GOAL]
case inr.inl
ι : Sort u_1
α : Type u
β : Type v
inst✝ : PseudoEMetricSpace α
δ✝ ε✝ : ℝ
s✝ t : Set α
x : α
ε δ : ℝ
s : Set α
hε : 0 ≤ ε
hδ : δ ≤ 0
⊢ thickening ε (thickening δ s) ⊆ thickening (ε + δ) s
[PROOFSTEP]
simp only [thickening_of_nonpos hδ, thickening_empty, empty_subset]
[GOAL]
case inr.inr
ι : Sort u_1
α : Type u
β : Type v
inst✝ : PseudoEMetricSpace α
δ✝ ε✝ : ℝ
s✝ t : Set α
x : α
ε δ : ℝ
s : Set α
hε : 0 ≤ ε
hδ : 0 ≤ δ
⊢ thickening ε (thickening δ s) ⊆ thickening (ε + δ) s
[PROOFSTEP]
intro x
[GOAL]
case inr.inr
ι : Sort u_1
α : Type u
β : Type v
inst✝ : PseudoEMetricSpace α
δ✝ ε✝ : ℝ
s✝ t : Set α
x✝ : α
ε δ : ℝ
s : Set α
hε : 0 ≤ ε
hδ : 0 ≤ δ
x : α
⊢ x ∈ thickening ε (thickening δ s) → x ∈ thickening (ε + δ) s
[PROOFSTEP]
simp_rw [mem_thickening_iff_exists_edist_lt, ENNReal.ofReal_add hε hδ]
[GOAL]
case inr.inr
ι : Sort u_1
α : Type u
β : Type v
inst✝ : PseudoEMetricSpace α
δ✝ ε✝ : ℝ
s✝ t : Set α
x✝ : α
ε δ : ℝ
s : Set α
hε : 0 ≤ ε
hδ : 0 ≤ δ
x : α
⊢ (∃ z, (∃ z_1, z_1 ∈ s ∧ edist z z_1 < ENNReal.ofReal δ) ∧ edist x z < ENNReal.ofReal ε) →
    ∃ z, z ∈ s ∧ edist x z < ENNReal.ofReal ε + ENNReal.ofReal δ
[PROOFSTEP]
exact fun ⟨y, ⟨z, hz, hy⟩, hx⟩ => ⟨z, hz, (edist_triangle _ _ _).trans_lt <| ENNReal.add_lt_add hx hy⟩
[GOAL]
ι : Sort u_1
α : Type u
β : Type v
inst✝ : PseudoEMetricSpace α
δ ε✝ : ℝ
s✝ t : Set α
x : α
ε : ℝ
hδ : 0 ≤ δ
s : Set α
⊢ thickening ε (cthickening δ s) ⊆ thickening (ε + δ) s
[PROOFSTEP]
obtain hε | hε := le_total ε 0
[GOAL]
case inl
ι : Sort u_1
α : Type u
β : Type v
inst✝ : PseudoEMetricSpace α
δ ε✝ : ℝ
s✝ t : Set α
x : α
ε : ℝ
hδ : 0 ≤ δ
s : Set α
hε : ε ≤ 0
⊢ thickening ε (cthickening δ s) ⊆ thickening (ε + δ) s
[PROOFSTEP]
simp only [thickening_of_nonpos hε, empty_subset]
[GOAL]
case inr
ι : Sort u_1
α : Type u
β : Type v
inst✝ : PseudoEMetricSpace α
δ ε✝ : ℝ
s✝ t : Set α
x : α
ε : ℝ
hδ : 0 ≤ δ
s : Set α
hε : 0 ≤ ε
⊢ thickening ε (cthickening δ s) ⊆ thickening (ε + δ) s
[PROOFSTEP]
intro x
[GOAL]
case inr
ι : Sort u_1
α : Type u
β : Type v
inst✝ : PseudoEMetricSpace α
δ ε✝ : ℝ
s✝ t : Set α
x✝ : α
ε : ℝ
hδ : 0 ≤ δ
s : Set α
hε : 0 ≤ ε
x : α
⊢ x ∈ thickening ε (cthickening δ s) → x ∈ thickening (ε + δ) s
[PROOFSTEP]
simp_rw [mem_thickening_iff_exists_edist_lt, mem_cthickening_iff, ← infEdist_lt_iff, ENNReal.ofReal_add hε hδ]
[GOAL]
case inr
ι : Sort u_1
α : Type u
β : Type v
inst✝ : PseudoEMetricSpace α
δ ε✝ : ℝ
s✝ t : Set α
x✝ : α
ε : ℝ
hδ : 0 ≤ δ
s : Set α
hε : 0 ≤ ε
x : α
⊢ (∃ z, infEdist z s ≤ ENNReal.ofReal δ ∧ edist x z < ENNReal.ofReal ε) →
    infEdist x s < ENNReal.ofReal ε + ENNReal.ofReal δ
[PROOFSTEP]
rintro ⟨y, hy, hxy⟩
[GOAL]
case inr.intro.intro
ι : Sort u_1
α : Type u
β : Type v
inst✝ : PseudoEMetricSpace α
δ ε✝ : ℝ
s✝ t : Set α
x✝ : α
ε : ℝ
hδ : 0 ≤ δ
s : Set α
hε : 0 ≤ ε
x y : α
hy : infEdist y s ≤ ENNReal.ofReal δ
hxy : edist x y < ENNReal.ofReal ε
⊢ infEdist x s < ENNReal.ofReal ε + ENNReal.ofReal δ
[PROOFSTEP]
exact
  infEdist_le_edist_add_infEdist.trans_lt (ENNReal.add_lt_add_of_lt_of_le (hy.trans_lt ENNReal.ofReal_lt_top).ne hxy hy)
[GOAL]
ι : Sort u_1
α : Type u
β : Type v
inst✝ : PseudoEMetricSpace α
δ✝ ε : ℝ
s✝ t : Set α
x : α
hε : 0 ≤ ε
δ : ℝ
s : Set α
⊢ cthickening ε (thickening δ s) ⊆ cthickening (ε + δ) s
[PROOFSTEP]
obtain hδ | hδ := le_total δ 0
[GOAL]
case inl
ι : Sort u_1
α : Type u
β : Type v
inst✝ : PseudoEMetricSpace α
δ✝ ε : ℝ
s✝ t : Set α
x : α
hε : 0 ≤ ε
δ : ℝ
s : Set α
hδ : δ ≤ 0
⊢ cthickening ε (thickening δ s) ⊆ cthickening (ε + δ) s
[PROOFSTEP]
simp only [thickening_of_nonpos hδ, cthickening_empty, empty_subset]
[GOAL]
case inr
ι : Sort u_1
α : Type u
β : Type v
inst✝ : PseudoEMetricSpace α
δ✝ ε : ℝ
s✝ t : Set α
x : α
hε : 0 ≤ ε
δ : ℝ
s : Set α
hδ : 0 ≤ δ
⊢ cthickening ε (thickening δ s) ⊆ cthickening (ε + δ) s
[PROOFSTEP]
intro x
[GOAL]
case inr
ι : Sort u_1
α : Type u
β : Type v
inst✝ : PseudoEMetricSpace α
δ✝ ε : ℝ
s✝ t : Set α
x✝ : α
hε : 0 ≤ ε
δ : ℝ
s : Set α
hδ : 0 ≤ δ
x : α
⊢ x ∈ cthickening ε (thickening δ s) → x ∈ cthickening (ε + δ) s
[PROOFSTEP]
simp_rw [mem_cthickening_iff, ENNReal.ofReal_add hε hδ]
[GOAL]
case inr
ι : Sort u_1
α : Type u
β : Type v
inst✝ : PseudoEMetricSpace α
δ✝ ε : ℝ
s✝ t : Set α
x✝ : α
hε : 0 ≤ ε
δ : ℝ
s : Set α
hδ : 0 ≤ δ
x : α
⊢ infEdist x (thickening δ s) ≤ ENNReal.ofReal ε → infEdist x s ≤ ENNReal.ofReal ε + ENNReal.ofReal δ
[PROOFSTEP]
exact fun hx => infEdist_le_infEdist_thickening_add.trans (add_le_add_right hx _)
[GOAL]
ι : Sort u_1
α : Type u
β : Type v
inst✝ : PseudoEMetricSpace α
δ ε : ℝ
s✝ t : Set α
x : α
hε : 0 ≤ ε
hδ : 0 ≤ δ
s : Set α
⊢ cthickening ε (cthickening δ s) ⊆ cthickening (ε + δ) s
[PROOFSTEP]
intro x
[GOAL]
ι : Sort u_1
α : Type u
β : Type v
inst✝ : PseudoEMetricSpace α
δ ε : ℝ
s✝ t : Set α
x✝ : α
hε : 0 ≤ ε
hδ : 0 ≤ δ
s : Set α
x : α
⊢ x ∈ cthickening ε (cthickening δ s) → x ∈ cthickening (ε + δ) s
[PROOFSTEP]
simp_rw [mem_cthickening_iff, ENNReal.ofReal_add hε hδ]
[GOAL]
ι : Sort u_1
α : Type u
β : Type v
inst✝ : PseudoEMetricSpace α
δ ε : ℝ
s✝ t : Set α
x✝ : α
hε : 0 ≤ ε
hδ : 0 ≤ δ
s : Set α
x : α
⊢ infEdist x (cthickening δ s) ≤ ENNReal.ofReal ε → infEdist x s ≤ ENNReal.ofReal ε + ENNReal.ofReal δ
[PROOFSTEP]
exact fun hx => infEdist_le_infEdist_cthickening_add.trans (add_le_add_right hx _)
[GOAL]
ι : Sort u_1
α : Type u
β : Type v
inst✝ : PseudoEMetricSpace α
δ ε : ℝ
s t : Set α
x : α
A : Set α
r₁ r₂ : ℝ≥0
hr : r₁ ≠ r₂
⊢ ENNReal.ofReal ↑r₁ ≠ ENNReal.ofReal ↑r₂
[PROOFSTEP]
simpa
