α : Type u
inst✝ : EMetricSpace α
s : Set α
hs : IsClosed s
t : Closeds α
ht : t ∈ closure {t | ↑t ⊆ s}
x : α
hx : x ∈ ↑t
⊢ x ∈ s
α : Type u
inst✝ : EMetricSpace α
s : Set α
hs : IsClosed s
⊢ IsClosed {t | ↑t ⊆ s}
refine' isClosed_of_closure_subset fun t ht x hx => _
α : Type u
inst✝ : EMetricSpace α
s : Set α
hs : IsClosed s
t : Closeds α
ht : t ∈ closure {t | ↑t ⊆ s}
x : α
hx : x ∈ ↑t
this : x ∈ closure s
⊢ x ∈ s
α : Type u
inst✝ : EMetricSpace α
s : Set α
hs : IsClosed s
t : Closeds α
ht : t ∈ closure {t | ↑t ⊆ s}
x : α
hx : x ∈ ↑t
⊢ x ∈ s
have : x ∈ closure s := by
  refine' mem_closure_iff.2 fun ε εpos => _
  rcases mem_closure_iff.1 ht ε εpos with ⟨u, hu, Dtu⟩
  rcases exists_edist_lt_of_hausdorffEdist_lt hx Dtu with ⟨y, hy, Dxy⟩
  exact ⟨y, hu hy, Dxy⟩
no goals
α : Type u
inst✝ : EMetricSpace α
s : Set α
hs : IsClosed s
t : Closeds α
ht : t ∈ closure {t | ↑t ⊆ s}
x : α
hx : x ∈ ↑t
this : x ∈ closure s
⊢ x ∈ s
rwa [hs.closure_eq] at this
α : Type u
inst✝ : EMetricSpace α
s : Set α
hs : IsClosed s
t : Closeds α
ht : t ∈ closure {t | ↑t ⊆ s}
x : α
hx : x ∈ ↑t
ε : ℝ≥0∞
εpos : ε > 0
⊢ ∃ y, y ∈ s ∧ edist x y < ε
α : Type u
inst✝ : EMetricSpace α
s : Set α
hs : IsClosed s
t : Closeds α
ht : t ∈ closure {t | ↑t ⊆ s}
x : α
hx : x ∈ ↑t
⊢ x ∈ closure s
refine' mem_closure_iff.2 fun ε εpos => _
case intro.intro
α : Type u
inst✝ : EMetricSpace α
s : Set α
hs : IsClosed s
t : Closeds α
ht : t ∈ closure {t | ↑t ⊆ s}
x : α
hx : x ∈ ↑t
ε : ℝ≥0∞
εpos : ε > 0
u : Closeds α
hu : u ∈ {t | ↑t ⊆ s}
Dtu : edist t u < ε
⊢ ∃ y, y ∈ s ∧ edist x y < ε
α : Type u
inst✝ : EMetricSpace α
s : Set α
hs : IsClosed s
t : Closeds α
ht : t ∈ closure {t | ↑t ⊆ s}
x : α
hx : x ∈ ↑t
ε : ℝ≥0∞
εpos : ε > 0
⊢ ∃ y, y ∈ s ∧ edist x y < ε
rcases mem_closure_iff.1 ht ε εpos with ⟨u, hu, Dtu⟩
case intro.intro.intro.intro
α : Type u
inst✝ : EMetricSpace α
s : Set α
hs : IsClosed s
t : Closeds α
ht : t ∈ closure {t | ↑t ⊆ s}
x : α
hx : x ∈ ↑t
ε : ℝ≥0∞
εpos : ε > 0
u : Closeds α
hu : u ∈ {t | ↑t ⊆ s}
Dtu : edist t u < ε
y : α
hy : y ∈ ↑u
Dxy : edist x y < ε
⊢ ∃ y, y ∈ s ∧ edist x y < ε
case intro.intro
α : Type u
inst✝ : EMetricSpace α
s : Set α
hs : IsClosed s
t : Closeds α
ht : t ∈ closure {t | ↑t ⊆ s}
x : α
hx : x ∈ ↑t
ε : ℝ≥0∞
εpos : ε > 0
u : Closeds α
hu : u ∈ {t | ↑t ⊆ s}
Dtu : edist t u < ε
⊢ ∃ y, y ∈ s ∧ edist x y < ε
rcases exists_edist_lt_of_hausdorffEdist_lt hx Dtu with ⟨y, hy, Dxy⟩
no goals
case intro.intro.intro.intro
α : Type u
inst✝ : EMetricSpace α
s : Set α
hs : IsClosed s
t : Closeds α
ht : t ∈ closure {t | ↑t ⊆ s}
x : α
hx : x ∈ ↑t
ε : ℝ≥0∞
εpos : ε > 0
u : Closeds α
hu : u ∈ {t | ↑t ⊆ s}
Dtu : edist t u < ε
y : α
hy : y ∈ ↑u
Dxy : edist x y < ε
⊢ ∃ y, y ∈ s ∧ edist x y < ε
exact ⟨y, hu hy, Dxy⟩