Locally finite families

A locally finite family of sets stays locally finite when it is reindexed along the first projection ι × κ → ι with κ finite (LocallyFinite.comp_fst), and more generally along (Σ i, κ i) → ι with every κ i finite (LocallyFinite.comp_sigma_fst). Together with LocallyFinite.subset, this makes a family indexed by ι × κ whose (i, k)-th member lies in the i-th member of a locally finite family locally finite. Dually, the pointwise union of finitely many locally finite families is locally finite (LocallyFinite.iUnion), as is the family of all pairwise intersections of two locally finite families (LocallyFinite.inter). A compact set has a neighbourhood meeting only finitely many members of a locally finite family (LocallyFinite.exists_mem_nhdsSet_finite), so the images of the members under a closed map with compact fibres, such as a proper map, again form a locally finite family (LocallyFinite.image_of_isClosedMap). The topological support of a locally finite sum of functions lies in the union of their topological supports (LocallyFinite.tsupport_finsum_subset).

In a pseudometric space, a locally finite family of closed sets has the following useful local description: around each point there is a ball such that every member of the family meeting the ball contains the centre.

On a normal paracompact space, positive continuous functions on the members of a locally finite closed family admit a single positive continuous strict minorant. This allows local error tolerances to be assembled without a uniform lower bound on a noncompact space. The minorant is constructed with Mathlib's exists_continuous_forall_mem_convex_of_local_const.

theorem LocallyFinite.comp_sigma_fst {ι : Type u_1} {X : Type u_3} [TopologicalSpace X] {f : ι → Set X} {κ : ι → Type u_4} [∀ (i : ι), Finite (κ i)] (hf : LocallyFinite f) : LocallyFinite fun (p : (i : ι) × κ i) => f p.fst

A locally finite family stays locally finite when reindexed along the first projection (Σ i, κ i) → ι, for finite fibres κ i.

theorem LocallyFinite.comp_fst {ι : Type u_1} {κ : Type u_2} {X : Type u_3} [TopologicalSpace X] {f : ι → Set X} [Finite κ] (hf : LocallyFinite f) : LocallyFinite fun (p : ι × κ) => f p.1

A locally finite family stays locally finite when reindexed along the first projection ι × κ → ι, for κ finite.

theorem LocallyFinite.inter {ι : Type u_1} {κ : Type u_2} {X : Type u_3} [TopologicalSpace X] {s : ι → Set X} {t : κ → Set X} (hs : LocallyFinite s) (ht : LocallyFinite t) : LocallyFinite fun (p : ι × κ) => s p.1 ∩ t p.2

The pairwise intersections of two locally finite families form a locally finite family. The index set includes all pairs, whether or not the two families are the same.

theorem LocallyFinite.exists_continuous_pos_lt {ι : Type u_1} {X : Type u_3} [TopologicalSpace X] {f : ι → Set X} [NormalSpace X] [ParacompactSpace X] (hf : LocallyFinite f) (hclosed : ∀ (i : ι), IsClosed (f i)) {ε : ι → X → ℝ} (hε : ∀ (i : ι), ContinuousOn (ε i) (f i)) (hpos : ∀ (i : ι), ∀ x ∈ f i, 0 < ε i x) : ∃ (δ : C(X, ℝ)), (∀ (x : X), 0 < δ x) ∧ ∀ (i : ι), ∀ x ∈ f i, δ x < ε i x

Positive continuous tolerances on a locally finite family of closed sets admit a positive continuous strict minorant on the whole space. No covering or compactness assumption is needed.

theorem LocallyFinite.iUnion {ι : Type u_1} {κ : Type u_2} {X : Type u_3} [TopologicalSpace X] [Finite κ] {f : κ → ι → Set X} (hf : ∀ (k : κ), LocallyFinite (f k)) : LocallyFinite fun (i : ι) => ⋃ (k : κ), f k i

The pointwise union of finitely many locally finite families is locally finite.

theorem LocallyFinite.exists_mem_nhdsSet_finite {ι : Type u_1} {X : Type u_3} [TopologicalSpace X] {f : ι → Set X} (hf : LocallyFinite f) {K : Set X} (hK : IsCompact K) : ∃ W ∈ nhdsSet K, {i : ι | (f i ∩ W).Nonempty}.Finite

A locally finite family has, around every compact set, a neighbourhood meeting only finitely many of its members.

theorem LocallyFinite.image_of_isClosedMap {ι : Type u_1} {X : Type u_3} [TopologicalSpace X] {f : ι → Set X} {Y : Type u_4} [TopologicalSpace Y] {g : X → Y} (hf : LocallyFinite f) (hg : IsClosedMap g) (hfib : ∀ (y : Y), IsCompact (g ⁻¹' {y})) : LocallyFinite fun (i : ι) => g '' f i

The image of a locally finite family under a closed map with compact fibres is locally finite. This applies in particular to proper maps.

theorem LocallyFinite.mulTSupport_finprod_subset {ι : Type u_1} {X : Type u_3} [TopologicalSpace X] {M : Type u_4} [CommMonoid M] {b : ι → X → M} (hb : LocallyFinite fun (i : ι) => Function.mulSupport (b i)) : (mulTSupport fun (x : X) => ∏ᶠ (i : ι), b i x) ⊆ ⋃ (i : ι), mulTSupport (b i)

The topological multiplicative support of a product of functions with locally finite multiplicative supports lies in the union of their topological multiplicative supports.

theorem LocallyFinite.tsupport_finsum_subset {ι : Type u_1} {X : Type u_3} [TopologicalSpace X] {M : Type u_4} [AddCommMonoid M] {b : ι → X → M} (hb : LocallyFinite fun (i : ι) => Function.support (b i)) : (tsupport fun (x : X) => ∑ᶠ (i : ι), b i x) ⊆ ⋃ (i : ι), tsupport (b i)

The topological support of a sum of functions with locally finite supports lies in the union of their topological supports.

theorem TauCeti.exists_pos_forall_mem_of_mem_ball {X : Type u_1} {ι : Type u_2} [PseudoMetricSpace X] {s : ι → Set X} (hs : ∀ (i : ι), IsClosed (s i)) (hlf : LocallyFinite s) (x : X) : ∃ r > 0, ∀ (i : ι), ∀ y ∈ Metric.ball x r, y ∈ s i → x ∈ s i

Around each point there is a ball such that every member of a locally finite family of closed sets that meets the ball contains the centre.