English
If f is subordinate to an open cover U = (U_i) by a family of open sets, then around any point x there is a finite index set I and a neighborhood N of x such that N ⊆ ∩_{i∈I} U_i and for every z ∈ N the support of the function x ↦ f_i(z) is contained in I.
Русский
Если f подпадает под открытое покрытие U = (U_i) семейством открытых множеств, то около любой точки x существует конечный индексный набор I и окрестность N(x) такая, что N ⊆ ⋂_{i∈I} U_i и для каждого z ∈ N опорa функции z ↦ f_i(z) содержится в I.
LaTeX
$$$$\exists I \subseteq ι,\ I \text{ finite},\ \exists n \in 𝓝(x),\ n \subseteq \bigcap_{i\in I} U_i \\ \\ \forall z \in n,\ \mathrm{supp}(f \cdot z) \subseteq I.$$$$
Lean4
theorem exists_finset_nhds_support_subset {U : ι → Set X} (hso : f.IsSubordinate U) (ho : ∀ i, IsOpen (U i)) (x : X) :
∃ is : Finset ι, ∃ n ∈ 𝓝 x, n ⊆ ⋂ i ∈ is, U i ∧ ∀ z ∈ n, (support (f · z)) ⊆ is :=
f.locallyFinite.exists_finset_nhds_support_subset hso ho x
