case intro.intro.intro
α : Type u
β : Type v
inst✝⁴ : TopologicalSpace α
γ : Type ?u.141701
inst✝³ : TopologicalSpace β
inst✝² : TopologicalSpace γ
inst✝¹ : LocallyCompactSpace α
inst✝ : T2Space α
K U : Set α
hK : IsCompact K
hU : IsOpen U
hKU : K ⊆ U
V : Set α
hV : IsCompact V
hKV : K ⊆ interior V
hVU : V ⊆ U
⊢ ∃ V, IsOpen V ∧ K ⊆ V ∧ closure V ⊆ U ∧ IsCompact (closure V)
α : Type u
β : Type v
inst✝⁴ : TopologicalSpace α
γ : Type ?u.141701
inst✝³ : TopologicalSpace β
inst✝² : TopologicalSpace γ
inst✝¹ : LocallyCompactSpace α
inst✝ : T2Space α
K U : Set α
hK : IsCompact K
hU : IsOpen U
hKU : K ⊆ U
⊢ ∃ V, IsOpen V ∧ K ⊆ V ∧ closure V ⊆ U ∧ IsCompact (closure V)
rcases exists_compact_between hK hU hKU with ⟨V, hV, hKV, hVU⟩
no goals
case intro.intro.intro
α : Type u
β : Type v
inst✝⁴ : TopologicalSpace α
γ : Type ?u.141701
inst✝³ : TopologicalSpace β
inst✝² : TopologicalSpace γ
inst✝¹ : LocallyCompactSpace α
inst✝ : T2Space α
K U : Set α
hK : IsCompact K
hU : IsOpen U
hKU : K ⊆ U
V : Set α
hV : IsCompact V
hKV : K ⊆ interior V
hVU : V ⊆ U
⊢ ∃ V, IsOpen V ∧ K ⊆ V ∧ closure V ⊆ U ∧ IsCompact (closure V)
exact
  ⟨interior V, isOpen_interior, hKV, (closure_minimal interior_subset hV.isClosed).trans hVU,
    isCompact_closure_of_subset_compact hV interior_subset⟩