α : Type u_1
β : Type ?u.836440
γ : Type ?u.836443
δ : Type ?u.836446
ι : Type ?u.836449
R : Type ?u.836452
R' : Type ?u.836455
m0 : MeasurableSpace α
inst✝⁴ : MeasurableSpace β
inst✝³ : MeasurableSpace γ
μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s s' t : Set α
inst✝² : TopologicalSpace α
inst✝¹ : LocallyCompactSpace α
inst✝ : IsFiniteMeasureOnCompacts μ
x : α
⊢ FiniteAtFilter μ (𝓝 x)
α : Type u_1
β : Type ?u.836440
γ : Type ?u.836443
δ : Type ?u.836446
ι : Type ?u.836449
R : Type ?u.836452
R' : Type ?u.836455
m0 : MeasurableSpace α
inst✝⁴ : MeasurableSpace β
inst✝³ : MeasurableSpace γ
μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s s' t : Set α
inst✝² : TopologicalSpace α
inst✝¹ : LocallyCompactSpace α
inst✝ : IsFiniteMeasureOnCompacts μ
⊢ ∀ (x : α), FiniteAtFilter μ (𝓝 x)
intro x
case intro.intro
α : Type u_1
β : Type ?u.836440
γ : Type ?u.836443
δ : Type ?u.836446
ι : Type ?u.836449
R : Type ?u.836452
R' : Type ?u.836455
m0 : MeasurableSpace α
inst✝⁴ : MeasurableSpace β
inst✝³ : MeasurableSpace γ
μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s s' t : Set α
inst✝² : TopologicalSpace α
inst✝¹ : LocallyCompactSpace α
inst✝ : IsFiniteMeasureOnCompacts μ
x : α
K : Set α
K_compact : IsCompact K
K_mem : K ∈ 𝓝 x
⊢ FiniteAtFilter μ (𝓝 x)
α : Type u_1
β : Type ?u.836440
γ : Type ?u.836443
δ : Type ?u.836446
ι : Type ?u.836449
R : Type ?u.836452
R' : Type ?u.836455
m0 : MeasurableSpace α
inst✝⁴ : MeasurableSpace β
inst✝³ : MeasurableSpace γ
μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s s' t : Set α
inst✝² : TopologicalSpace α
inst✝¹ : LocallyCompactSpace α
inst✝ : IsFiniteMeasureOnCompacts μ
x : α
⊢ FiniteAtFilter μ (𝓝 x)
rcases exists_compact_mem_nhds x with ⟨K, K_compact, K_mem⟩
no goals
case intro.intro
α : Type u_1
β : Type ?u.836440
γ : Type ?u.836443
δ : Type ?u.836446
ι : Type ?u.836449
R : Type ?u.836452
R' : Type ?u.836455
m0 : MeasurableSpace α
inst✝⁴ : MeasurableSpace β
inst✝³ : MeasurableSpace γ
μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s s' t : Set α
inst✝² : TopologicalSpace α
inst✝¹ : LocallyCompactSpace α
inst✝ : IsFiniteMeasureOnCompacts μ
x : α
K : Set α
K_compact : IsCompact K
K_mem : K ∈ 𝓝 x
⊢ FiniteAtFilter μ (𝓝 x)
exact ⟨K, K_mem, K_compact.measure_lt_top⟩