case inl
ι : Sort ?u.28317
α : 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

case inr
ι : Sort ?u.28317
α : 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
ι : Sort ?u.28317
α : 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
rcases s.eq_empty_or_nonempty with (rfl | hne)
case inr.intro.intro
ι : Sort ?u.28317
α : 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
case inr
ι : Sort ?u.28317
α : 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
obtain ⟨x, hx, h⟩ : ∃ x ∈ s, ∀ y ∈ s, infEdist x t ≤ infEdist y t :=
  hs.exists_forall_le hne continuous_infEdist.continuousOn
case inr.intro.intro
ι : Sort ?u.28317
α : 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
case inr.intro.intro
ι : Sort ?u.28317
α : 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
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⟩
case inr.intro.intro.intro.intro
ι : Sort ?u.28317
α : 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
case inr.intro.intro
ι : Sort ?u.28317
α : 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
rcases ENNReal.lt_iff_exists_nnreal_btwn.1 this with ⟨r, h₀, hr⟩
no goals
case inr.intro.intro.intro.intro
ι : Sort ?u.28317
α : 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
exact ⟨r, ENNReal.coe_pos.mp h₀, fun y hy z hz => hr.trans_le <| le_infEdist.1 (h y hy) z hz⟩
case inl
ι : Sort ?u.28317
α : 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
case inl
ι : Sort ?u.28317
α : 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
use 1
no goals
case inl
ι : Sort ?u.28317
α : 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
simp