case intro.intro.intro
α : Type u
β : Type v
X : Type ?u.313712
inst✝¹ : PseudoEMetricSpace α
γ : Type w
inst✝ : EMetricSpace γ
s : Set γ
hs : IsCompact s
t : Set γ
hts : t ⊆ s
htc : Set.Countable t
hsub : s ⊆ closure t
⊢ ∃ t, t ⊆ s ∧ Set.Countable t ∧ s = closure t
α : Type u
β : Type v
X : Type ?u.313712
inst✝¹ : PseudoEMetricSpace α
γ : Type w
inst✝ : EMetricSpace γ
s : Set γ
hs : IsCompact s
⊢ ∃ t, t ⊆ s ∧ Set.Countable t ∧ s = closure t
rcases subset_countable_closure_of_compact hs with ⟨t, hts, htc, hsub⟩
no goals
case intro.intro.intro
α : Type u
β : Type v
X : Type ?u.313712
inst✝¹ : PseudoEMetricSpace α
γ : Type w
inst✝ : EMetricSpace γ
s : Set γ
hs : IsCompact s
t : Set γ
hts : t ⊆ s
htc : Set.Countable t
hsub : s ⊆ closure t
⊢ ∃ t, t ⊆ s ∧ Set.Countable t ∧ s = closure t
exact ⟨t, hts, htc, hsub.antisymm (closure_minimal hts hs.isClosed)⟩