α : Type u
inst✝¹ : EMetricSpace α
s : Set α
inst✝ : CompleteSpace α
this : range NonemptyCompacts.toCloseds = {s | Set.Nonempty ↑s ∧ IsCompact ↑s}
⊢ IsClosed (range NonemptyCompacts.toCloseds)
α : Type u
inst✝¹ : EMetricSpace α
s : Set α
inst✝ : CompleteSpace α
⊢ IsClosed (range NonemptyCompacts.toCloseds)
have :
  range NonemptyCompacts.toCloseds =
    { s : Closeds α | (s : Set α).Nonempty ∧ IsCompact (s : Set α) } := by
  ext s
  refine' ⟨_, fun h => ⟨⟨⟨s, h.2⟩, h.1⟩, Closeds.ext rfl⟩⟩
  rintro ⟨s, hs, rfl⟩
  exact ⟨s.nonempty, s.isCompact⟩
α : Type u
inst✝¹ : EMetricSpace α
s : Set α
inst✝ : CompleteSpace α
this : range NonemptyCompacts.toCloseds = {s | Set.Nonempty ↑s ∧ IsCompact ↑s}
⊢ IsClosed {s | Set.Nonempty ↑s ∧ IsCompact ↑s}
α : Type u
inst✝¹ : EMetricSpace α
s : Set α
inst✝ : CompleteSpace α
this : range NonemptyCompacts.toCloseds = {s | Set.Nonempty ↑s ∧ IsCompact ↑s}
⊢ IsClosed (range NonemptyCompacts.toCloseds)
rw [this]
case refine'_1
α : Type u
inst✝¹ : EMetricSpace α
s✝ : Set α
inst✝ : CompleteSpace α
this : range NonemptyCompacts.toCloseds = {s | Set.Nonempty ↑s ∧ IsCompact ↑s}
s : Closeds α
hs : s ∈ closure {s | Set.Nonempty ↑s ∧ IsCompact ↑s}
⊢ Set.Nonempty ↑s

case refine'_2
α : Type u
inst✝¹ : EMetricSpace α
s✝ : Set α
inst✝ : CompleteSpace α
this : range NonemptyCompacts.toCloseds = {s | Set.Nonempty ↑s ∧ IsCompact ↑s}
s : Closeds α
hs : s ∈ closure {s | Set.Nonempty ↑s ∧ IsCompact ↑s}
⊢ IsCompact ↑s
α : Type u
inst✝¹ : EMetricSpace α
s : Set α
inst✝ : CompleteSpace α
this : range NonemptyCompacts.toCloseds = {s | Set.Nonempty ↑s ∧ IsCompact ↑s}
⊢ IsClosed {s | Set.Nonempty ↑s ∧ IsCompact ↑s}
refine' isClosed_of_closure_subset fun s hs => ⟨_, _⟩
case h
α : Type u
inst✝¹ : EMetricSpace α
s✝ : Set α
inst✝ : CompleteSpace α
s : Closeds α
⊢ s ∈ range NonemptyCompacts.toCloseds ↔ s ∈ {s | Set.Nonempty ↑s ∧ IsCompact ↑s}
α : Type u
inst✝¹ : EMetricSpace α
s : Set α
inst✝ : CompleteSpace α
⊢ range NonemptyCompacts.toCloseds = {s | Set.Nonempty ↑s ∧ IsCompact ↑s}
ext s
case h
α : Type u
inst✝¹ : EMetricSpace α
s✝ : Set α
inst✝ : CompleteSpace α
s : Closeds α
⊢ s ∈ range NonemptyCompacts.toCloseds → s ∈ {s | Set.Nonempty ↑s ∧ IsCompact ↑s}
case h
α : Type u
inst✝¹ : EMetricSpace α
s✝ : Set α
inst✝ : CompleteSpace α
s : Closeds α
⊢ s ∈ range NonemptyCompacts.toCloseds ↔ s ∈ {s | Set.Nonempty ↑s ∧ IsCompact ↑s}
refine' ⟨_, fun h => ⟨⟨⟨s, h.2⟩, h.1⟩, Closeds.ext rfl⟩⟩
case h.intro.refl
α : Type u
inst✝¹ : EMetricSpace α
s✝ : Set α
inst✝ : CompleteSpace α
s : NonemptyCompacts α
⊢ NonemptyCompacts.toCloseds s ∈ {s | Set.Nonempty ↑s ∧ IsCompact ↑s}
case h
α : Type u
inst✝¹ : EMetricSpace α
s✝ : Set α
inst✝ : CompleteSpace α
s : Closeds α
⊢ s ∈ range NonemptyCompacts.toCloseds → s ∈ {s | Set.Nonempty ↑s ∧ IsCompact ↑s}
rintro ⟨s, hs, rfl⟩
no goals
case h.intro.refl
α : Type u
inst✝¹ : EMetricSpace α
s✝ : Set α
inst✝ : CompleteSpace α
s : NonemptyCompacts α
⊢ NonemptyCompacts.toCloseds s ∈ {s | Set.Nonempty ↑s ∧ IsCompact ↑s}
exact ⟨s.nonempty, s.isCompact⟩
case refine'_1.intro.intro
α : Type u
inst✝¹ : EMetricSpace α
s✝ : Set α
inst✝ : CompleteSpace α
this : range NonemptyCompacts.toCloseds = {s | Set.Nonempty ↑s ∧ IsCompact ↑s}
s : Closeds α
hs : s ∈ closure {s | Set.Nonempty ↑s ∧ IsCompact ↑s}
t : Closeds α
ht : t ∈ {s | Set.Nonempty ↑s ∧ IsCompact ↑s}
Dst : edist s t < ⊤
⊢ Set.Nonempty ↑s
case refine'_1
α : Type u
inst✝¹ : EMetricSpace α
s✝ : Set α
inst✝ : CompleteSpace α
this : range NonemptyCompacts.toCloseds = {s | Set.Nonempty ↑s ∧ IsCompact ↑s}
s : Closeds α
hs : s ∈ closure {s | Set.Nonempty ↑s ∧ IsCompact ↑s}
⊢ Set.Nonempty ↑s
rcases mem_closure_iff.1 hs ⊤ ENNReal.coe_lt_top with ⟨t, ht, Dst⟩
case refine'_1.intro.intro
α : Type u
inst✝¹ : EMetricSpace α
s✝ : Set α
inst✝ : CompleteSpace α
this : range NonemptyCompacts.toCloseds = {s | Set.Nonempty ↑s ∧ IsCompact ↑s}
s : Closeds α
hs : s ∈ closure {s | Set.Nonempty ↑s ∧ IsCompact ↑s}
t : Closeds α
ht : t ∈ {s | Set.Nonempty ↑s ∧ IsCompact ↑s}
Dst : edist t s < ⊤
⊢ Set.Nonempty ↑s
case refine'_1.intro.intro
α : Type u
inst✝¹ : EMetricSpace α
s✝ : Set α
inst✝ : CompleteSpace α
this : range NonemptyCompacts.toCloseds = {s | Set.Nonempty ↑s ∧ IsCompact ↑s}
s : Closeds α
hs : s ∈ closure {s | Set.Nonempty ↑s ∧ IsCompact ↑s}
t : Closeds α
ht : t ∈ {s | Set.Nonempty ↑s ∧ IsCompact ↑s}
Dst : edist s t < ⊤
⊢ Set.Nonempty ↑s
rw [edist_comm] at Dst
no goals
case refine'_1.intro.intro
α : Type u
inst✝¹ : EMetricSpace α
s✝ : Set α
inst✝ : CompleteSpace α
this : range NonemptyCompacts.toCloseds = {s | Set.Nonempty ↑s ∧ IsCompact ↑s}
s : Closeds α
hs : s ∈ closure {s | Set.Nonempty ↑s ∧ IsCompact ↑s}
t : Closeds α
ht : t ∈ {s | Set.Nonempty ↑s ∧ IsCompact ↑s}
Dst : edist t s < ⊤
⊢ Set.Nonempty ↑s
exact nonempty_of_hausdorffEdist_ne_top ht.1 (ne_of_lt Dst)
case refine'_2
α : Type u
inst✝¹ : EMetricSpace α
s✝ : Set α
inst✝ : CompleteSpace α
this : range NonemptyCompacts.toCloseds = {s | Set.Nonempty ↑s ∧ IsCompact ↑s}
s : Closeds α
hs : s ∈ closure {s | Set.Nonempty ↑s ∧ IsCompact ↑s}
⊢ TotallyBounded ↑s
case refine'_2
α : Type u
inst✝¹ : EMetricSpace α
s✝ : Set α
inst✝ : CompleteSpace α
this : range NonemptyCompacts.toCloseds = {s | Set.Nonempty ↑s ∧ IsCompact ↑s}
s : Closeds α
hs : s ∈ closure {s | Set.Nonempty ↑s ∧ IsCompact ↑s}
⊢ IsCompact ↑s
refine' isCompact_iff_totallyBounded_isComplete.2 ⟨_, s.closed.isComplete⟩
case refine'_2
α : Type u
inst✝¹ : EMetricSpace α
s✝ : Set α
inst✝ : CompleteSpace α
this : range NonemptyCompacts.toCloseds = {s | Set.Nonempty ↑s ∧ IsCompact ↑s}
s : Closeds α
hs : s ∈ closure {s | Set.Nonempty ↑s ∧ IsCompact ↑s}
ε : ℝ≥0∞
εpos : 0 < ε
⊢ ∃ t, Set.Finite t ∧ ↑s ⊆ ⋃ (y : α) (_ : y ∈ t), ball y ε
case refine'_2
α : Type u
inst✝¹ : EMetricSpace α
s✝ : Set α
inst✝ : CompleteSpace α
this : range NonemptyCompacts.toCloseds = {s | Set.Nonempty ↑s ∧ IsCompact ↑s}
s : Closeds α
hs : s ∈ closure {s | Set.Nonempty ↑s ∧ IsCompact ↑s}
⊢ TotallyBounded ↑s
refine' totallyBounded_iff.2 fun ε (εpos : 0 < ε) => _
case refine'_2.intro.intro
α : Type u
inst✝¹ : EMetricSpace α
s✝ : Set α
inst✝ : CompleteSpace α
this : range NonemptyCompacts.toCloseds = {s | Set.Nonempty ↑s ∧ IsCompact ↑s}
s : Closeds α
hs : s ∈ closure {s | Set.Nonempty ↑s ∧ IsCompact ↑s}
ε : ℝ≥0∞
εpos : 0 < ε
t : Closeds α
ht : t ∈ {s | Set.Nonempty ↑s ∧ IsCompact ↑s}
Dst : edist s t < ε / 2
⊢ ∃ t, Set.Finite t ∧ ↑s ⊆ ⋃ (y : α) (_ : y ∈ t), ball y ε
case refine'_2
α : Type u
inst✝¹ : EMetricSpace α
s✝ : Set α
inst✝ : CompleteSpace α
this : range NonemptyCompacts.toCloseds = {s | Set.Nonempty ↑s ∧ IsCompact ↑s}
s : Closeds α
hs : s ∈ closure {s | Set.Nonempty ↑s ∧ IsCompact ↑s}
ε : ℝ≥0∞
εpos : 0 < ε
⊢ ∃ t, Set.Finite t ∧ ↑s ⊆ ⋃ (y : α) (_ : y ∈ t), ball y ε
rcases mem_closure_iff.1 hs (ε / 2) (ENNReal.half_pos εpos.ne') with ⟨t, ht, Dst⟩
case refine'_2.intro.intro.intro.intro
α : Type u
inst✝¹ : EMetricSpace α
s✝ : Set α
inst✝ : CompleteSpace α
this : range NonemptyCompacts.toCloseds = {s | Set.Nonempty ↑s ∧ IsCompact ↑s}
s : Closeds α
hs : s ∈ closure {s | Set.Nonempty ↑s ∧ IsCompact ↑s}
ε : ℝ≥0∞
εpos : 0 < ε
t : Closeds α
ht : t ∈ {s | Set.Nonempty ↑s ∧ IsCompact ↑s}
Dst : edist s t < ε / 2
u : Set α
fu : Set.Finite u
ut : ↑t ⊆ ⋃ (y : α) (_ : y ∈ u), ball y (ε / 2)
⊢ ∃ t, Set.Finite t ∧ ↑s ⊆ ⋃ (y : α) (_ : y ∈ t), ball y ε
case refine'_2.intro.intro
α : Type u
inst✝¹ : EMetricSpace α
s✝ : Set α
inst✝ : CompleteSpace α
this : range NonemptyCompacts.toCloseds = {s | Set.Nonempty ↑s ∧ IsCompact ↑s}
s : Closeds α
hs : s ∈ closure {s | Set.Nonempty ↑s ∧ IsCompact ↑s}
ε : ℝ≥0∞
εpos : 0 < ε
t : Closeds α
ht : t ∈ {s | Set.Nonempty ↑s ∧ IsCompact ↑s}
Dst : edist s t < ε / 2
⊢ ∃ t, Set.Finite t ∧ ↑s ⊆ ⋃ (y : α) (_ : y ∈ t), ball y ε
rcases totallyBounded_iff.1 (isCompact_iff_totallyBounded_isComplete.1 ht.2).1 (ε / 2)
    (ENNReal.half_pos εpos.ne') with
  ⟨u, fu, ut⟩
case refine'_2.intro.intro.intro.intro
α : Type u
inst✝¹ : EMetricSpace α
s✝ : Set α
inst✝ : CompleteSpace α
this : range NonemptyCompacts.toCloseds = {s | Set.Nonempty ↑s ∧ IsCompact ↑s}
s : Closeds α
hs : s ∈ closure {s | Set.Nonempty ↑s ∧ IsCompact ↑s}
ε : ℝ≥0∞
εpos : 0 < ε
t : Closeds α
ht : t ∈ {s | Set.Nonempty ↑s ∧ IsCompact ↑s}
Dst : edist s t < ε / 2
u : Set α
fu : Set.Finite u
ut : ↑t ⊆ ⋃ (y : α) (_ : y ∈ u), ball y (ε / 2)
x : α
hx : x ∈ ↑s
⊢ x ∈ ⋃ (y : α) (_ : y ∈ u), ball y ε
case refine'_2.intro.intro.intro.intro
α : Type u
inst✝¹ : EMetricSpace α
s✝ : Set α
inst✝ : CompleteSpace α
this : range NonemptyCompacts.toCloseds = {s | Set.Nonempty ↑s ∧ IsCompact ↑s}
s : Closeds α
hs : s ∈ closure {s | Set.Nonempty ↑s ∧ IsCompact ↑s}
ε : ℝ≥0∞
εpos : 0 < ε
t : Closeds α
ht : t ∈ {s | Set.Nonempty ↑s ∧ IsCompact ↑s}
Dst : edist s t < ε / 2
u : Set α
fu : Set.Finite u
ut : ↑t ⊆ ⋃ (y : α) (_ : y ∈ u), ball y (ε / 2)
⊢ ∃ t, Set.Finite t ∧ ↑s ⊆ ⋃ (y : α) (_ : y ∈ t), ball y ε
refine' ⟨u, ⟨fu, fun x hx => _⟩⟩
case refine'_2.intro.intro.intro.intro.intro.intro
α : Type u
inst✝¹ : EMetricSpace α
s✝ : Set α
inst✝ : CompleteSpace α
this : range NonemptyCompacts.toCloseds = {s | Set.Nonempty ↑s ∧ IsCompact ↑s}
s : Closeds α
hs : s ∈ closure {s | Set.Nonempty ↑s ∧ IsCompact ↑s}
ε : ℝ≥0∞
εpos : 0 < ε
t : Closeds α
ht : t ∈ {s | Set.Nonempty ↑s ∧ IsCompact ↑s}
Dst : edist s t < ε / 2
u : Set α
fu : Set.Finite u
ut : ↑t ⊆ ⋃ (y : α) (_ : y ∈ u), ball y (ε / 2)
x : α
hx : x ∈ ↑s
z : α
hz : z ∈ ↑t
Dxz : edist x z < ε / 2
⊢ x ∈ ⋃ (y : α) (_ : y ∈ u), ball y ε
case refine'_2.intro.intro.intro.intro
α : Type u
inst✝¹ : EMetricSpace α
s✝ : Set α
inst✝ : CompleteSpace α
this : range NonemptyCompacts.toCloseds = {s | Set.Nonempty ↑s ∧ IsCompact ↑s}
s : Closeds α
hs : s ∈ closure {s | Set.Nonempty ↑s ∧ IsCompact ↑s}
ε : ℝ≥0∞
εpos : 0 < ε
t : Closeds α
ht : t ∈ {s | Set.Nonempty ↑s ∧ IsCompact ↑s}
Dst : edist s t < ε / 2
u : Set α
fu : Set.Finite u
ut : ↑t ⊆ ⋃ (y : α) (_ : y ∈ u), ball y (ε / 2)
x : α
hx : x ∈ ↑s
⊢ x ∈ ⋃ (y : α) (_ : y ∈ u), ball y ε
rcases exists_edist_lt_of_hausdorffEdist_lt hx Dst with ⟨z, hz, Dxz⟩
case refine'_2.intro.intro.intro.intro.intro.intro.intro.intro
α : Type u
inst✝¹ : EMetricSpace α
s✝ : Set α
inst✝ : CompleteSpace α
this : range NonemptyCompacts.toCloseds = {s | Set.Nonempty ↑s ∧ IsCompact ↑s}
s : Closeds α
hs : s ∈ closure {s | Set.Nonempty ↑s ∧ IsCompact ↑s}
ε : ℝ≥0∞
εpos : 0 < ε
t : Closeds α
ht : t ∈ {s | Set.Nonempty ↑s ∧ IsCompact ↑s}
Dst : edist s t < ε / 2
u : Set α
fu : Set.Finite u
ut : ↑t ⊆ ⋃ (y : α) (_ : y ∈ u), ball y (ε / 2)
x : α
hx : x ∈ ↑s
z : α
hz : z ∈ ↑t
Dxz : edist x z < ε / 2
y : α
hy : y ∈ u
Dzy : z ∈ ball y (ε / 2)
⊢ x ∈ ⋃ (y : α) (_ : y ∈ u), ball y ε
case refine'_2.intro.intro.intro.intro.intro.intro
α : Type u
inst✝¹ : EMetricSpace α
s✝ : Set α
inst✝ : CompleteSpace α
this : range NonemptyCompacts.toCloseds = {s | Set.Nonempty ↑s ∧ IsCompact ↑s}
s : Closeds α
hs : s ∈ closure {s | Set.Nonempty ↑s ∧ IsCompact ↑s}
ε : ℝ≥0∞
εpos : 0 < ε
t : Closeds α
ht : t ∈ {s | Set.Nonempty ↑s ∧ IsCompact ↑s}
Dst : edist s t < ε / 2
u : Set α
fu : Set.Finite u
ut : ↑t ⊆ ⋃ (y : α) (_ : y ∈ u), ball y (ε / 2)
x : α
hx : x ∈ ↑s
z : α
hz : z ∈ ↑t
Dxz : edist x z < ε / 2
⊢ x ∈ ⋃ (y : α) (_ : y ∈ u), ball y ε
rcases mem_iUnion₂.1 (ut hz) with ⟨y, hy, Dzy⟩
case refine'_2.intro.intro.intro.intro.intro.intro.intro.intro
α : Type u
inst✝¹ : EMetricSpace α
s✝ : Set α
inst✝ : CompleteSpace α
this✝ : range NonemptyCompacts.toCloseds = {s | Set.Nonempty ↑s ∧ IsCompact ↑s}
s : Closeds α
hs : s ∈ closure {s | Set.Nonempty ↑s ∧ IsCompact ↑s}
ε : ℝ≥0∞
εpos : 0 < ε
t : Closeds α
ht : t ∈ {s | Set.Nonempty ↑s ∧ IsCompact ↑s}
Dst : edist s t < ε / 2
u : Set α
fu : Set.Finite u
ut : ↑t ⊆ ⋃ (y : α) (_ : y ∈ u), ball y (ε / 2)
x : α
hx : x ∈ ↑s
z : α
hz : z ∈ ↑t
Dxz : edist x z < ε / 2
y : α
hy : y ∈ u
Dzy : z ∈ ball y (ε / 2)
this : edist x y < ε
⊢ x ∈ ⋃ (y : α) (_ : y ∈ u), ball y ε
case refine'_2.intro.intro.intro.intro.intro.intro.intro.intro
α : Type u
inst✝¹ : EMetricSpace α
s✝ : Set α
inst✝ : CompleteSpace α
this : range NonemptyCompacts.toCloseds = {s | Set.Nonempty ↑s ∧ IsCompact ↑s}
s : Closeds α
hs : s ∈ closure {s | Set.Nonempty ↑s ∧ IsCompact ↑s}
ε : ℝ≥0∞
εpos : 0 < ε
t : Closeds α
ht : t ∈ {s | Set.Nonempty ↑s ∧ IsCompact ↑s}
Dst : edist s t < ε / 2
u : Set α
fu : Set.Finite u
ut : ↑t ⊆ ⋃ (y : α) (_ : y ∈ u), ball y (ε / 2)
x : α
hx : x ∈ ↑s
z : α
hz : z ∈ ↑t
Dxz : edist x z < ε / 2
y : α
hy : y ∈ u
Dzy : z ∈ ball y (ε / 2)
⊢ x ∈ ⋃ (y : α) (_ : y ∈ u), ball y ε
have : edist x y < ε :=
  calc
    edist x y ≤ edist x z + edist z y := edist_triangle _ _ _
    _ < ε / 2 + ε / 2 := (ENNReal.add_lt_add Dxz Dzy)
    _ = ε := ENNReal.add_halves _
no goals
case refine'_2.intro.intro.intro.intro.intro.intro.intro.intro
α : Type u
inst✝¹ : EMetricSpace α
s✝ : Set α
inst✝ : CompleteSpace α
this✝ : range NonemptyCompacts.toCloseds = {s | Set.Nonempty ↑s ∧ IsCompact ↑s}
s : Closeds α
hs : s ∈ closure {s | Set.Nonempty ↑s ∧ IsCompact ↑s}
ε : ℝ≥0∞
εpos : 0 < ε
t : Closeds α
ht : t ∈ {s | Set.Nonempty ↑s ∧ IsCompact ↑s}
Dst : edist s t < ε / 2
u : Set α
fu : Set.Finite u
ut : ↑t ⊆ ⋃ (y : α) (_ : y ∈ u), ball y (ε / 2)
x : α
hx : x ∈ ↑s
z : α
hz : z ∈ ↑t
Dxz : edist x z < ε / 2
y : α
hy : y ∈ u
Dzy : z ∈ ball y (ε / 2)
this : edist x y < ε
⊢ x ∈ ⋃ (y : α) (_ : y ∈ u), ball y ε
exact mem_biUnion hy this