case intro.intro
ι : Type u_2
α : Type ?u.448737
X : Type u_3
M✝ : Type ?u.448743
N : Type ?u.448746
inst✝⁴ : TopologicalSpace X
inst✝³ : TopologicalSpace M✝
inst✝² : CommMonoid M✝
inst✝¹ : ContinuousMul M✝
M : Type u_1
inst✝ : CommMonoid M
f : ι → X → M
hf : LocallyFinite fun i => mulSupport (f i)
x₀ : X
U : Set X
hxU : U ∈ 𝓝 x₀
hUf : Set.Finite {i | Set.Nonempty ((fun i => mulSupport (f i)) i ∩ U)}
⊢ ∃ I, ∀ᶠ (x : X) in 𝓝 x₀, (mulSupport fun i => f i x) ⊆ ↑I
ι : Type u_2
α : Type ?u.448737
X : Type u_3
M✝ : Type ?u.448743
N : Type ?u.448746
inst✝⁴ : TopologicalSpace X
inst✝³ : TopologicalSpace M✝
inst✝² : CommMonoid M✝
inst✝¹ : ContinuousMul M✝
M : Type u_1
inst✝ : CommMonoid M
f : ι → X → M
hf : LocallyFinite fun i => mulSupport (f i)
x₀ : X
⊢ ∃ I, ∀ᶠ (x : X) in 𝓝 x₀, (mulSupport fun i => f i x) ⊆ ↑I
rcases hf x₀ with ⟨U, hxU, hUf⟩
case intro.intro
ι : Type u_2
α : Type ?u.448737
X : Type u_3
M✝ : Type ?u.448743
N : Type ?u.448746
inst✝⁴ : TopologicalSpace X
inst✝³ : TopologicalSpace M✝
inst✝² : CommMonoid M✝
inst✝¹ : ContinuousMul M✝
M : Type u_1
inst✝ : CommMonoid M
f : ι → X → M
hf : LocallyFinite fun i => mulSupport (f i)
x₀ : X
U : Set X
hxU : U ∈ 𝓝 x₀
hUf : Set.Finite {i | Set.Nonempty ((fun i => mulSupport (f i)) i ∩ U)}
y : X
hy : y ∈ U
i : ι
hi : i ∈ mulSupport fun i => f i y
⊢ i ∈ ↑(Finite.toFinset hUf)
case intro.intro
ι : Type u_2
α : Type ?u.448737
X : Type u_3
M✝ : Type ?u.448743
N : Type ?u.448746
inst✝⁴ : TopologicalSpace X
inst✝³ : TopologicalSpace M✝
inst✝² : CommMonoid M✝
inst✝¹ : ContinuousMul M✝
M : Type u_1
inst✝ : CommMonoid M
f : ι → X → M
hf : LocallyFinite fun i => mulSupport (f i)
x₀ : X
U : Set X
hxU : U ∈ 𝓝 x₀
hUf : Set.Finite {i | Set.Nonempty ((fun i => mulSupport (f i)) i ∩ U)}
⊢ ∃ I, ∀ᶠ (x : X) in 𝓝 x₀, (mulSupport fun i => f i x) ⊆ ↑I
refine' ⟨hUf.toFinset, mem_of_superset hxU fun y hy i hi => _⟩
case intro.intro
ι : Type u_2
α : Type ?u.448737
X : Type u_3
M✝ : Type ?u.448743
N : Type ?u.448746
inst✝⁴ : TopologicalSpace X
inst✝³ : TopologicalSpace M✝
inst✝² : CommMonoid M✝
inst✝¹ : ContinuousMul M✝
M : Type u_1
inst✝ : CommMonoid M
f : ι → X → M
hf : LocallyFinite fun i => mulSupport (f i)
x₀ : X
U : Set X
hxU : U ∈ 𝓝 x₀
hUf : Set.Finite {i | Set.Nonempty ((fun i => mulSupport (f i)) i ∩ U)}
y : X
hy : y ∈ U
i : ι
hi : i ∈ mulSupport fun i => f i y
⊢ i ∈ {i | Set.Nonempty ((fun i => mulSupport (f i)) i ∩ U)}
case intro.intro
ι : Type u_2
α : Type ?u.448737
X : Type u_3
M✝ : Type ?u.448743
N : Type ?u.448746
inst✝⁴ : TopologicalSpace X
inst✝³ : TopologicalSpace M✝
inst✝² : CommMonoid M✝
inst✝¹ : ContinuousMul M✝
M : Type u_1
inst✝ : CommMonoid M
f : ι → X → M
hf : LocallyFinite fun i => mulSupport (f i)
x₀ : X
U : Set X
hxU : U ∈ 𝓝 x₀
hUf : Set.Finite {i | Set.Nonempty ((fun i => mulSupport (f i)) i ∩ U)}
y : X
hy : y ∈ U
i : ι
hi : i ∈ mulSupport fun i => f i y
⊢ i ∈ ↑(Finite.toFinset hUf)
rw [hUf.coe_toFinset]
no goals
case intro.intro
ι : Type u_2
α : Type ?u.448737
X : Type u_3
M✝ : Type ?u.448743
N : Type ?u.448746
inst✝⁴ : TopologicalSpace X
inst✝³ : TopologicalSpace M✝
inst✝² : CommMonoid M✝
inst✝¹ : ContinuousMul M✝
M : Type u_1
inst✝ : CommMonoid M
f : ι → X → M
hf : LocallyFinite fun i => mulSupport (f i)
x₀ : X
U : Set X
hxU : U ∈ 𝓝 x₀
hUf : Set.Finite {i | Set.Nonempty ((fun i => mulSupport (f i)) i ∩ U)}
y : X
hy : y ∈ U
i : ι
hi : i ∈ mulSupport fun i => f i y
⊢ i ∈ {i | Set.Nonempty ((fun i => mulSupport (f i)) i ∩ U)}
exact ⟨y, hi, hy⟩