English
If a family has locally finite multiplicative support subordinate to open sets U_i, then for any x there exists a finite index set and a neighborhood of x contained in the intersection of those open sets such that only finitely many indices appear in the supports within that neighborhood.
Русский
Если семейство имеет локально конечную мультиподдержку, подчинённую открытым множествам U_i, то для любой точки x можно найти конечный подмножество индексов и окрестность x, содержащуюся в их пересечении, внутри которой в поддержках задействованы лишь эти индексы.
LaTeX
$$$\exists \text{is} : \Finset ι,\ \exists n \in 𝓝 x,\ n \subseteq \bigcap_{i\in \text{is}} U_i \land \forall z \in n,\ \operatorname{mulSupport}(\lambda i. f_i(z)) \subseteq \text{is}.$$$
Lean4
/-- If a family of functions `f` has locally-finite multiplicative support, subordinate to a family
of open sets, then for any point we can find a neighbourhood on which only finitely-many members of
`f` are not equal to 1. -/
@[to_additive /-- If a family of functions `f` has locally-finite support, subordinate to a family
of open sets, then for any point we can find a neighbourhood on which only finitely-many members of
`f` are non-zero. -/
]
theorem exists_finset_nhds_mulSupport_subset {U : ι → Set X} [One R] {f : ι → X → R}
(hlf : LocallyFinite fun i => mulSupport (f i)) (hso : ∀ i, mulTSupport (f i) ⊆ U i) (ho : ∀ i, IsOpen (U i))
(x : X) : ∃ (is : Finset ι), ∃ n, n ∈ 𝓝 x ∧ (n ⊆ ⋂ i ∈ is, U i) ∧ ∀ z ∈ n, (mulSupport fun i => f i z) ⊆ is :=
by
obtain ⟨n, hn, hnf⟩ := hlf x
classical
let is := {i ∈ hnf.toFinset | x ∈ U i}
let js := {j ∈ hnf.toFinset | x ∉ U j}
refine
⟨is, (n ∩ ⋂ j ∈ js, (mulTSupport (f j))ᶜ) ∩ ⋂ i ∈ is, U i, inter_mem (inter_mem hn ?_) ?_, inter_subset_right,
fun z hz => ?_⟩
·
exact
(biInter_finset_mem js).mpr fun j hj =>
IsClosed.compl_mem_nhds (isClosed_mulTSupport _) (Set.notMem_subset (hso j) (Finset.mem_filter.mp hj).2)
· exact (biInter_finset_mem is).mpr fun i hi => (ho i).mem_nhds (Finset.mem_filter.mp hi).2
· have hzn : z ∈ n := by
rw [inter_assoc] at hz
exact mem_of_mem_inter_left hz
replace hz := mem_of_mem_inter_right (mem_of_mem_inter_left hz)
simp only [js, Finset.mem_filter, Finite.mem_toFinset, mem_setOf_eq, mem_iInter, and_imp] at hz
suffices (mulSupport fun i => f i z) ⊆ hnf.toFinset
by
refine hnf.toFinset.subset_coe_filter_of_subset_forall _ this fun i hi => ?_
specialize hz i ⟨z, ⟨hi, hzn⟩⟩
contrapose hz
simp [hz, subset_mulTSupport (f i) hi]
intro i hi
simp only [Finite.coe_toFinset, mem_setOf_eq]
exact ⟨z, ⟨hi, hzn⟩⟩
