α : Type u_1
E : Type u_2
ι : Type ?u.898853
hm : MeasurableSpace α
μ : MeasureTheory.Measure α
inst✝⁷ : TopologicalSpace α
inst✝⁶ : BorelSpace α
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
g : α → E
l : Filter ι
x₀ : α
s : Set α
φ : ι → α → ℝ
inst✝³ : CompleteSpace E
inst✝² : MetrizableSpace α
inst✝¹ : IsLocallyFiniteMeasure μ
inst✝ : IsOpenPosMeasure μ
hs : IsCompact s
c : α → ℝ
hc : ContinuousOn c s
h'c : ∀ (y : α), y ∈ s → y ≠ x₀ → c y < c x₀
hnc : ∀ (x : α), x ∈ s → 0 ≤ c x
hnc₀ : 0 < c x₀
h₀ : x₀ ∈ closure (interior s)
hmg : ContinuousOn g s
⊢ x₀ ∈ closure s
α : Type u_1
E : Type u_2
ι : Type ?u.898853
hm : MeasurableSpace α
μ : MeasureTheory.Measure α
inst✝⁷ : TopologicalSpace α
inst✝⁶ : BorelSpace α
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
g : α → E
l : Filter ι
x₀ : α
s : Set α
φ : ι → α → ℝ
inst✝³ : CompleteSpace E
inst✝² : MetrizableSpace α
inst✝¹ : IsLocallyFiniteMeasure μ
inst✝ : IsOpenPosMeasure μ
hs : IsCompact s
c : α → ℝ
hc : ContinuousOn c s
h'c : ∀ (y : α), y ∈ s → y ≠ x₀ → c y < c x₀
hnc : ∀ (x : α), x ∈ s → 0 ≤ c x
hnc₀ : 0 < c x₀
h₀ : x₀ ∈ closure (interior s)
hmg : ContinuousOn g s
⊢ x₀ ∈ s
rw [← hs.isClosed.closure_eq]
no goals
α : Type u_1
E : Type u_2
ι : Type ?u.898853
hm : MeasurableSpace α
μ : MeasureTheory.Measure α
inst✝⁷ : TopologicalSpace α
inst✝⁶ : BorelSpace α
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
g : α → E
l : Filter ι
x₀ : α
s : Set α
φ : ι → α → ℝ
inst✝³ : CompleteSpace E
inst✝² : MetrizableSpace α
inst✝¹ : IsLocallyFiniteMeasure μ
inst✝ : IsOpenPosMeasure μ
hs : IsCompact s
c : α → ℝ
hc : ContinuousOn c s
h'c : ∀ (y : α), y ∈ s → y ≠ x₀ → c y < c x₀
hnc : ∀ (x : α), x ∈ s → 0 ≤ c x
hnc₀ : 0 < c x₀
h₀ : x₀ ∈ closure (interior s)
hmg : ContinuousOn g s
⊢ x₀ ∈ closure s
exact closure_mono interior_subset h₀