Mathlib.Topology.LocallyFinite

LocallyFinite definition

(f : ι → Set X)

Full source

/-- A family of sets in `Set X` is locally finite if at every point `x : X`,
there is a neighborhood of `x` which meets only finitely many sets in the family. -/
def LocallyFinite (f : ι → Set X) :=
  ∀ x : X, ∃ t ∈ 𝓝 x, { i | (f i ∩ t).Nonempty }.Finite

Locally finite family of sets

Informal description

A family of sets $\{f_i\}_{i \in \iota}$ in a topological space $X$ is called *locally finite* if for every point $x \in X$, there exists a neighborhood $t$ of $x$ such that the set $\{i \in \iota \mid f_i \cap t \neq \emptyset\}$ is finite.

locallyFinite_of_finite theorem

[Finite ι] (f : ι → Set X) : LocallyFinite f

Full source

theorem locallyFinite_of_finite [Finite ι] (f : ι → Set X) : LocallyFinite f := fun _ =>
  ⟨univ, univ_mem, toFinite _⟩

Finite families of sets are locally finite

Informal description

For any finite index set $\iota$ and any family of sets $\{f_i\}_{i \in \iota}$ in a topological space $X$, the family $\{f_i\}_{i \in \iota}$ is locally finite.

LocallyFinite.point_finite theorem

(hf : LocallyFinite f) (x : X) : {b | x ∈ f b}.Finite

Full source

theorem point_finite (hf : LocallyFinite f) (x : X) : { b | x ∈ f b }.Finite :=
  let ⟨_t, hxt, ht⟩ := hf x
  ht.subset fun _b hb => ⟨x, hb, mem_of_mem_nhds hxt⟩

Finiteness of Indices at a Point for Locally Finite Families

Informal description

Let $\{f_i\}_{i \in \iota}$ be a locally finite family of sets in a topological space $X$. Then for any point $x \in X$, the set $\{i \in \iota \mid x \in f_i\}$ is finite.

LocallyFinite.subset theorem

(hf : LocallyFinite f) (hg : ∀ i, g i ⊆ f i) : LocallyFinite g

Full source

protected theorem subset (hf : LocallyFinite f) (hg : ∀ i, g i ⊆ f i) : LocallyFinite g := fun a =>
  let ⟨t, ht₁, ht₂⟩ := hf a
  ⟨t, ht₁, ht₂.subset fun i hi => hi.mono <| inter_subset_inter (hg i) Subset.rfl⟩

Subfamilies of Locally Finite Families are Locally Finite

Informal description

Let $\{f_i\}_{i \in \iota}$ be a locally finite family of sets in a topological space $X$. If $\{g_i\}_{i \in \iota}$ is another family of sets such that $g_i \subseteq f_i$ for every $i \in \iota$, then $\{g_i\}_{i \in \iota}$ is also locally finite.

LocallyFinite.comp_injOn theorem

{g : ι' → ι} (hf : LocallyFinite f) (hg : InjOn g {i | (f (g i)).Nonempty}) : LocallyFinite (f ∘ g)

Full source

theorem comp_injOn {g : ι' → ι} (hf : LocallyFinite f) (hg : InjOn g { i | (f (g i)).Nonempty }) :
    LocallyFinite (f ∘ g) := fun x => by
  let ⟨t, htx, htf⟩ := hf x
  refine ⟨t, htx, htf.preimage <| ?_⟩
  exact hg.mono fun i (hi : Set.Nonempty _) => hi.left

Locally Finite Family under Injective Restriction of Indices

Informal description

Let $\{f_i\}_{i \in \iota}$ be a locally finite family of sets in a topological space $X$, and let $g : \iota' \to \iota$ be a function. If $g$ is injective on the set $\{i \in \iota' \mid f_{g(i)} \neq \emptyset\}$, then the family $\{f_{g(i)}\}_{i \in \iota'}$ is also locally finite.

LocallyFinite.comp_injective theorem

{g : ι' → ι} (hf : LocallyFinite f) (hg : Injective g) : LocallyFinite (f ∘ g)

Full source

theorem comp_injective {g : ι' → ι} (hf : LocallyFinite f) (hg : Injective g) :
    LocallyFinite (f ∘ g) :=
  hf.comp_injOn hg.injOn

Locally Finite Family under Injective Index Transformation

Informal description

Let $\{f_i\}_{i \in \iota}$ be a locally finite family of sets in a topological space $X$, and let $g : \iota' \to \iota$ be an injective function. Then the family $\{f_{g(i)}\}_{i \in \iota'}$ is also locally finite.

locallyFinite_iff_smallSets theorem

: LocallyFinite f ↔ ∀ x, ∀ᶠ s in (𝓝 x).smallSets, {i | (f i ∩ s).Nonempty}.Finite

Full source

theorem _root_.locallyFinite_iff_smallSets :
    LocallyFiniteLocallyFinite f ↔ ∀ x, ∀ᶠ s in (𝓝 x).smallSets, { i | (f i ∩ s).Nonempty }.Finite :=
  forall_congr' fun _ => Iff.symm <|
    eventually_smallSets' fun _s _t hst ht =>
      ht.subset fun _i hi => hi.mono <| inter_subset_inter_right _ hst

Characterization of Locally Finite Families via Neighborhood Bases

Informal description

A family of sets $\{f_i\}_{i \in \iota}$ in a topological space $X$ is locally finite if and only if for every point $x \in X$, there exists a neighborhood basis $\{s\}$ of $x$ such that the set $\{i \in \iota \mid f_i \cap s \neq \emptyset\}$ is finite for all $s$ in the basis.

LocallyFinite.eventually_smallSets theorem

(hf : LocallyFinite f) (x : X) : ∀ᶠ s in (𝓝 x).smallSets, {i | (f i ∩ s).Nonempty}.Finite

Full source

protected theorem eventually_smallSets (hf : LocallyFinite f) (x : X) :
    ∀ᶠ s in (𝓝 x).smallSets, { i | (f i ∩ s).Nonempty }.Finite :=
  locallyFinite_iff_smallSets.mp hf x

Neighborhood Condition for Locally Finite Families

Informal description

For a locally finite family of sets $\{f_i\}_{i \in \iota}$ in a topological space $X$ and any point $x \in X$, there exists a neighborhood $s$ of $x$ such that the set $\{i \in \iota \mid f_i \cap s \neq \emptyset\}$ is finite.

LocallyFinite.exists_mem_basis theorem

 {ι' : Sort*} (hf : LocallyFinite f) {p : ι' → Prop} {s : ι' → Set X} {x : X} (hb : (𝓝 x).HasBasis p s) :
  ∃ i, p i ∧ {j | (f j ∩ s i).Nonempty}.Finite

Full source

theorem exists_mem_basis {ι' : Sort*} (hf : LocallyFinite f) {p : ι' → Prop} {s : ι' → Set X}
    {x : X} (hb : (𝓝 x).HasBasis p s) : ∃ i, p i ∧ { j | (f j ∩ s i).Nonempty }.Finite :=
  let ⟨i, hpi, hi⟩ := hb.smallSets.eventually_iff.mp (hf.eventually_smallSets x)
  ⟨i, hpi, hi Subset.rfl⟩

Existence of Basis Neighborhood for Locally Finite Family

Informal description

Let $\{f_i\}_{i \in \iota}$ be a locally finite family of sets in a topological space $X$, and let $x \in X$. Suppose $\{s_j\}_{j \in \iota'}$ is a neighborhood basis of $x$ indexed by $\iota'$ with corresponding predicate $p$. Then there exists an index $j \in \iota'$ such that $p(j)$ holds and the set $\{i \in \iota \mid f_i \cap s_j \neq \emptyset\}$ is finite.

LocallyFinite.nhdsWithin_iUnion theorem

(hf : LocallyFinite f) (a : X) : 𝓝[⋃ i, f i] a = ⨆ i, 𝓝[f i] a

Full source

protected theorem nhdsWithin_iUnion (hf : LocallyFinite f) (a : X) :
    𝓝[⋃ i, f i] a = ⨆ i, 𝓝[f i] a := by
  rcases hf a with ⟨U, haU, hfin⟩
  refine le_antisymm ?_ (Monotone.le_map_iSup fun _ _ ↦ nhdsWithin_mono _)
  calc
    𝓝[⋃ i, f i] a = 𝓝[⋃ i, f i ∩ U] a := by
      rw [← iUnion_inter, ← nhdsWithin_inter_of_mem' (nhdsWithin_le_nhds haU)]
    _ = 𝓝[⋃ i ∈ {j | (f j ∩ U).Nonempty}, (f i ∩ U)] a := by
      simp only [mem_setOf_eq, iUnion_nonempty_self]
    _ = ⨆ i ∈ {j | (f j ∩ U).Nonempty}, 𝓝[f i ∩ U] a := nhdsWithin_biUnion hfin _ _
    _ ≤ ⨆ i, 𝓝[f i ∩ U] a := iSup₂_le_iSup _ _
    _ ≤ ⨆ i, 𝓝[f i] a := iSup_mono fun i ↦ nhdsWithin_mono _ inter_subset_left

Neighborhood Filter of Union for Locally Finite Family

Informal description

Let $\{f_i\}_{i \in \iota}$ be a locally finite family of sets in a topological space $X$. For any point $a \in X$, the neighborhood filter of $a$ within the union $\bigcup_i f_i$ is equal to the supremum of the neighborhood filters of $a$ within each individual set $f_i$. In symbols: $$ \mathcal{N}_{\bigcup_i f_i}(a) = \bigsqcup_i \mathcal{N}_{f_i}(a). $$

LocallyFinite.continuousOn_iUnion' theorem

 {g : X → Y} (hf : LocallyFinite f) (hc : ∀ i x, x ∈ closure (f i) → ContinuousWithinAt g (f i) x) :
  ContinuousOn g (⋃ i, f i)

Full source

theorem continuousOn_iUnion' {g : X → Y} (hf : LocallyFinite f)
    (hc : ∀ i x, x ∈ closure (f i) → ContinuousWithinAt g (f i) x) :
    ContinuousOn g (⋃ i, f i) := by
  rintro x -
  rw [ContinuousWithinAt, hf.nhdsWithin_iUnion, tendsto_iSup]
  intro i
  by_cases hx : x ∈ closure (f i)
  · exact hc i _ hx
  · rw [mem_closure_iff_nhdsWithin_neBot, not_neBot] at hx
    rw [hx]
    exact tendsto_bot

Continuity on Union for Locally Finite Family

Informal description

Let $\{f_i\}_{i \in \iota}$ be a locally finite family of sets in a topological space $X$, and let $g : X \to Y$ be a function. If for every index $i$ and every point $x$ in the closure of $f_i$, the function $g$ is continuous within $f_i$ at $x$, then $g$ is continuous on the union $\bigcup_i f_i$.

LocallyFinite.continuousOn_iUnion theorem

 {g : X → Y} (hf : LocallyFinite f) (h_cl : ∀ i, IsClosed (f i)) (h_cont : ∀ i, ContinuousOn g (f i)) :
  ContinuousOn g (⋃ i, f i)

Full source

theorem continuousOn_iUnion {g : X → Y} (hf : LocallyFinite f) (h_cl : ∀ i, IsClosed (f i))
    (h_cont : ∀ i, ContinuousOn g (f i)) : ContinuousOn g (⋃ i, f i) :=
  hf.continuousOn_iUnion' fun i x hx ↦ h_cont i x <| (h_cl i).closure_subset hx

Continuity on Union of Locally Finite Closed Family

Informal description

Let $\{f_i\}_{i \in \iota}$ be a locally finite family of closed sets in a topological space $X$, and let $g : X \to Y$ be a function. If for every index $i$, the function $g$ is continuous on $f_i$, then $g$ is continuous on the union $\bigcup_i f_i$.

LocallyFinite.continuous' theorem

 {g : X → Y} (hf : LocallyFinite f) (h_cov : ⋃ i, f i = univ)
  (hc : ∀ i x, x ∈ closure (f i) → ContinuousWithinAt g (f i) x) : Continuous g

Full source

protected theorem continuous' {g : X → Y} (hf : LocallyFinite f) (h_cov : ⋃ i, f i = univ)
    (hc : ∀ i x, x ∈ closure (f i) → ContinuousWithinAt g (f i) x) :
    Continuous g :=
  continuous_iff_continuousOn_univ.2 <| h_cov ▸ hf.continuousOn_iUnion' hc

Continuity via Local Finiteness and Pointwise Continuity on Closures

Informal description

Let $\{f_i\}_{i \in \iota}$ be a locally finite family of sets in a topological space $X$, and let $g : X \to Y$ be a function. Suppose that the union of all $f_i$ covers $X$ (i.e., $\bigcup_i f_i = X$), and for every index $i$ and every point $x$ in the closure of $f_i$, the function $g$ is continuous within $f_i$ at $x$. Then $g$ is continuous on $X$.

LocallyFinite.continuous theorem

 {g : X → Y} (hf : LocallyFinite f) (h_cov : ⋃ i, f i = univ) (h_cl : ∀ i, IsClosed (f i))
  (h_cont : ∀ i, ContinuousOn g (f i)) : Continuous g

Full source

protected theorem continuous {g : X → Y} (hf : LocallyFinite f) (h_cov : ⋃ i, f i = univ)
    (h_cl : ∀ i, IsClosed (f i)) (h_cont : ∀ i, ContinuousOn g (f i)) :
    Continuous g :=
  continuous_iff_continuousOn_univ.2 <| h_cov ▸ hf.continuousOn_iUnion h_cl h_cont

Continuity via Local Finiteness and Continuity on Closed Sets

Informal description

Let $\{f_i\}_{i \in \iota}$ be a locally finite family of closed sets in a topological space $X$ whose union is $X$, and let $g : X \to Y$ be a function. If for every index $i$, the function $g$ is continuous on $f_i$, then $g$ is continuous on $X$.

LocallyFinite.closure theorem

(hf : LocallyFinite f) : LocallyFinite fun i => closure (f i)

Full source

protected theorem closure (hf : LocallyFinite f) : LocallyFinite fun i => closure (f i) := by
  intro x
  rcases hf x with ⟨s, hsx, hsf⟩
  refine ⟨interior s, interior_mem_nhds.2 hsx, hsf.subset fun i hi => ?_⟩
  exact (hi.mono isOpen_interior.closure_inter).of_closure.mono
    (inter_subset_inter_right _ interior_subset)

Closure of a Locally Finite Family is Locally Finite

Informal description

If $\{f_i\}_{i \in \iota}$ is a locally finite family of sets in a topological space $X$, then the family of closures $\{\overline{f_i}\}_{i \in \iota}$ is also locally finite.

LocallyFinite.closure_iUnion theorem

(h : LocallyFinite f) : closure (⋃ i, f i) = ⋃ i, closure (f i)

Full source

theorem closure_iUnion (h : LocallyFinite f) : closure (⋃ i, f i) = ⋃ i, closure (f i) := by
  ext x
  simp only [mem_closure_iff_nhdsWithin_neBot, h.nhdsWithin_iUnion, iSup_neBot, mem_iUnion]

Closure of Union Equals Union of Closures for Locally Finite Family

Informal description

For a locally finite family of sets $\{f_i\}_{i \in \iota}$ in a topological space $X$, the closure of the union $\bigcup_i f_i$ is equal to the union of the closures $\bigcup_i \overline{f_i}$. In symbols: $$ \overline{\bigcup_i f_i} = \bigcup_i \overline{f_i}. $$

LocallyFinite.isClosed_iUnion theorem

(hf : LocallyFinite f) (hc : ∀ i, IsClosed (f i)) : IsClosed (⋃ i, f i)

Full source

theorem isClosed_iUnion (hf : LocallyFinite f) (hc : ∀ i, IsClosed (f i)) :
    IsClosed (⋃ i, f i) := by
  simp only [← closure_eq_iff_isClosed, hf.closure_iUnion, (hc _).closure_eq]

Union of Locally Finite Family of Closed Sets is Closed

Informal description

Let $\{f_i\}_{i \in \iota}$ be a locally finite family of closed sets in a topological space $X$. Then the union $\bigcup_i f_i$ is closed.

LocallyFinite.iInter_compl_mem_nhds theorem

(hf : LocallyFinite f) (hc : ∀ i, IsClosed (f i)) (x : X) : (⋂ (i) (_ : x ∉ f i), (f i)ᶜ) ∈ 𝓝 x

Full source

/-- If `f : β → Set α` is a locally finite family of closed sets, then for any `x : α`, the
intersection of the complements to `f i`, `x ∉ f i`, is a neighbourhood of `x`. -/
theorem iInter_compl_mem_nhds (hf : LocallyFinite f) (hc : ∀ i, IsClosed (f i)) (x : X) :
    (⋂ (i) (_ : x ∉ f i), (f i)ᶜ) ∈ 𝓝 x := by
  refine IsOpen.mem_nhds ?_ (mem_iInter₂.2 fun i => id)
  suffices IsClosed (⋃ i : { i // x ∉ f i }, f i) by
    rwa [← isOpen_compl_iff, compl_iUnion, iInter_subtype] at this
  exact (hf.comp_injective Subtype.val_injective).isClosed_iUnion fun i => hc _

Neighborhood Property for Complements of Locally Finite Closed Sets

Informal description

Let $\{f_i\}_{i \in \iota}$ be a locally finite family of closed sets in a topological space $X$. For any point $x \in X$, the intersection of the complements $\bigcap_{i : x \notin f_i} (f_i)^c$ is a neighborhood of $x$.

LocallyFinite.exists_forall_eventually_eq_prod theorem

 {π : X → Sort*} {f : ℕ → ∀ x : X, π x} (hf : LocallyFinite fun n => {x | f (n + 1) x ≠ f n x}) :
  ∃ F : ∀ x : X, π x, ∀ x, ∀ᶠ p : ℕ × X in atTop ×ˢ 𝓝 x, f p.1 p.2 = F p.2

Full source

/-- Let `f : ℕ → Π a, β a` be a sequence of (dependent) functions on a topological space. Suppose
that the family of sets `s n = {x | f (n + 1) x ≠ f n x}` is locally finite. Then there exists a
function `F : Π a, β a` such that for any `x`, we have `f n x = F x` on the product of an infinite
interval `[N, +∞)` and a neighbourhood of `x`.

We formulate the conclusion in terms of the product of filter `Filter.atTop` and `𝓝 x`. -/
theorem exists_forall_eventually_eq_prod {π : X → Sort*} {f : ℕ → ∀ x : X, π x}
    (hf : LocallyFinite fun n => { x | f (n + 1) x ≠ f n x }) :
    ∃ F : ∀ x : X, π x, ∀ x, ∀ᶠ p : ℕ × X in atTop ×ˢ 𝓝 x, f p.1 p.2 = F p.2 := by
  choose U hUx hU using hf
  choose N hN using fun x => (hU x).bddAbove
  replace hN : ∀ (x), ∀ n > N x, ∀ y ∈ U x, f (n + 1) y = f n y :=
    fun x n hn y hy => by_contra fun hne => hn.lt.not_le <| hN x ⟨y, hne, hy⟩
  replace hN : ∀ (x), ∀ n ≥ N x + 1, ∀ y ∈ U x, f n y = f (N x + 1) y :=
    fun x n hn y hy => Nat.le_induction rfl (fun k hle => (hN x _ hle _ hy).trans) n hn
  refine ⟨fun x => f (N x + 1) x, fun x => ?_⟩
  filter_upwards [Filter.prod_mem_prod (eventually_gt_atTop (N x)) (hUx x)]
  rintro ⟨n, y⟩ ⟨hn : N x < n, hy : y ∈ U x⟩
  calc
    f n y = f (N x + 1) y := hN _ _ hn _ hy
    _ = f (max (N x + 1) (N y + 1)) y := (hN _ _ (le_max_left _ _) _ hy).symm
    _ = f (N y + 1) y := hN _ _ (le_max_right _ _) _ (mem_of_mem_nhds <| hUx y)

Existence of Limit Function for Locally Finite Differences

Informal description

Let $X$ be a topological space and $\pi \colon X \to \text{Sort}^*$ be a dependent type family. Given a sequence of dependent functions $f_n \colon X \to \pi(x)$ for $n \in \mathbb{N}$, suppose the family of sets $\{x \in X \mid f_{n+1}(x) \neq f_n(x)\}$ is locally finite. Then there exists a function $F \colon X \to \pi(x)$ such that for every $x \in X$, the equality $f_n(y) = F(y)$ holds for all sufficiently large $n$ and all $y$ in some neighborhood of $x$.

LocallyFinite.exists_forall_eventually_atTop_eventually_eq' theorem

 {π : X → Sort*} {f : ℕ → ∀ x : X, π x} (hf : LocallyFinite fun n => {x | f (n + 1) x ≠ f n x}) :
  ∃ F : ∀ x : X, π x, ∀ x, ∀ᶠ n : ℕ in atTop, ∀ᶠ y : X in 𝓝 x, f n y = F y

Full source

/-- Let `f : ℕ → Π a, β a` be a sequence of (dependent) functions on a topological space. Suppose
that the family of sets `s n = {x | f (n + 1) x ≠ f n x}` is locally finite. Then there exists a
function `F : Π a, β a` such that for any `x`, for sufficiently large values of `n`, we have
`f n y = F y` in a neighbourhood of `x`. -/
theorem exists_forall_eventually_atTop_eventually_eq' {π : X → Sort*} {f : ℕ → ∀ x : X, π x}
    (hf : LocallyFinite fun n => { x | f (n + 1) x ≠ f n x }) :
    ∃ F : ∀ x : X, π x, ∀ x, ∀ᶠ n : ℕ in atTop, ∀ᶠ y : X in 𝓝 x, f n y = F y :=
  hf.exists_forall_eventually_eq_prod.imp fun _F hF x => (hF x).curry

Existence of Locally Uniform Limit for Functions with Locally Finite Differences

Informal description

Let $X$ be a topological space and $\pi \colon X \to \text{Sort}^*$ be a dependent type family. Given a sequence of dependent functions $f_n \colon X \to \pi(x)$ for $n \in \mathbb{N}$, suppose the family of sets $\{x \in X \mid f_{n+1}(x) \neq f_n(x)\}$ is locally finite. Then there exists a function $F \colon X \to \pi(x)$ such that for every $x \in X$, there exists $N \in \mathbb{N}$ and a neighborhood $U$ of $x$ such that for all $n \geq N$ and all $y \in U$, we have $f_n(y) = F(y)$.

LocallyFinite.exists_forall_eventually_atTop_eventuallyEq theorem

 {f : ℕ → X → α} (hf : LocallyFinite fun n => {x | f (n + 1) x ≠ f n x}) :
  ∃ F : X → α, ∀ x, ∀ᶠ n : ℕ in atTop, f n =ᶠ[𝓝 x] F

Full source

/-- Let `f : ℕ → α → β` be a sequence of functions on a topological space. Suppose
that the family of sets `s n = {x | f (n + 1) x ≠ f n x}` is locally finite. Then there exists a
function `F :  α → β` such that for any `x`, for sufficiently large values of `n`, we have
`f n =ᶠ[𝓝 x] F`. -/
theorem exists_forall_eventually_atTop_eventuallyEq {f : ℕ → X → α}
    (hf : LocallyFinite fun n => { x | f (n + 1) x ≠ f n x }) :
    ∃ F : X → α, ∀ x, ∀ᶠ n : ℕ in atTop, f n =ᶠ[𝓝 x] F :=
  hf.exists_forall_eventually_atTop_eventually_eq'

Existence of Local Uniform Limit for Functions with Locally Finite Differences

Informal description

Let $X$ be a topological space and $\{f_n\}_{n \in \mathbb{N}}$ be a sequence of functions $f_n \colon X \to \alpha$. Suppose the family of sets $\{x \in X \mid f_{n+1}(x) \neq f_n(x)\}$ is locally finite. Then there exists a function $F \colon X \to \alpha$ such that for every $x \in X$, the sequence $f_n$ eventually equals $F$ in a neighborhood of $x$ as $n \to \infty$.

LocallyFinite.preimage_continuous theorem

{g : Y → X} (hf : LocallyFinite f) (hg : Continuous g) : LocallyFinite (g ⁻¹' f ·)

Full source

theorem preimage_continuous {g : Y → X} (hf : LocallyFinite f) (hg : Continuous g) :
    LocallyFinite (g ⁻¹' f ·) := fun x =>
  let ⟨s, hsx, hs⟩ := hf (g x)
  ⟨g ⁻¹' s, hg.continuousAt hsx, hs.subset fun _ ⟨y, hy⟩ => ⟨g y, hy⟩⟩

Preimage of Locally Finite Family under Continuous Function is Locally Finite

Informal description

Let $X$ and $Y$ be topological spaces, and let $\{f_i\}_{i \in \iota}$ be a locally finite family of subsets of $X$. For any continuous function $g \colon Y \to X$, the family $\{g^{-1}(f_i)\}_{i \in \iota}$ is locally finite in $Y$.

LocallyFinite.prod_right theorem

(hf : LocallyFinite f) (g : ι → Set Y) : LocallyFinite (fun i ↦ f i ×ˢ g i)

Full source

theorem prod_right (hf : LocallyFinite f) (g : ι → Set Y) : LocallyFinite (fun i ↦ f i ×ˢ g i) :=
  (hf.preimage_continuous continuous_fst).subset fun _ ↦ prod_subset_preimage_fst _ _

Locally Finite Family Preserved under Right Product with Arbitrary Family

Informal description

Let $\{f_i\}_{i \in \iota}$ be a locally finite family of subsets of a topological space $X$, and let $\{g_i\}_{i \in \iota}$ be an arbitrary family of subsets of a topological space $Y$. Then the family $\{f_i \times g_i\}_{i \in \iota}$ is locally finite in the product space $X \times Y$.

LocallyFinite.prod_left theorem

{g : ι → Set Y} (hg : LocallyFinite g) (f : ι → Set X) : LocallyFinite (fun i ↦ f i ×ˢ g i)

Full source

theorem prod_left {g : ι → Set Y} (hg : LocallyFinite g) (f : ι → Set X) :
    LocallyFinite (fun i ↦ f i ×ˢ g i) :=
  (hg.preimage_continuous continuous_snd).subset fun _ ↦ prod_subset_preimage_snd _ _

Locally Finite Family under Left Product with Arbitrary Family

Informal description

Let $X$ and $Y$ be topological spaces, and let $\{g_i\}_{i \in \iota}$ be a locally finite family of subsets of $Y$. For any family of subsets $\{f_i\}_{i \in \iota}$ of $X$, the family of product sets $\{f_i \times g_i\}_{i \in \iota}$ is locally finite in $X \times Y$.

Equiv.locallyFinite_comp_iff theorem

(e : ι' ≃ ι) : LocallyFinite (f ∘ e) ↔ LocallyFinite f

Full source

@[simp]
theorem Equiv.locallyFinite_comp_iff (e : ι' ≃ ι) : LocallyFiniteLocallyFinite (f ∘ e) ↔ LocallyFinite f :=
  ⟨fun h => by simpa only [comp_def, e.apply_symm_apply] using h.comp_injective e.symm.injective,
    fun h => h.comp_injective e.injective⟩

Locally Finite Family under Index Bijection: $\{f_{e(i)}\}_{i \in \iota'}$ is locally finite iff $\{f_i\}_{i \in \iota}$ is locally finite

Informal description

Let $X$ be a topological space and $\{f_i\}_{i \in \iota}$ be a family of subsets of $X$. Given a bijection $e : \iota' \to \iota$, the family $\{f_{e(i')}\}_{i' \in \iota'}$ is locally finite if and only if the original family $\{f_i\}_{i \in \iota}$ is locally finite.

locallyFinite_sum theorem

{f : ι ⊕ ι' → Set X} : LocallyFinite f ↔ LocallyFinite (f ∘ Sum.inl) ∧ LocallyFinite (f ∘ Sum.inr)

Full source

theorem locallyFinite_sum {f : ι ⊕ ι' → Set X} :
    LocallyFiniteLocallyFinite f ↔ LocallyFinite (f ∘ Sum.inl) ∧ LocallyFinite (f ∘ Sum.inr) := by
  simp only [locallyFinite_iff_smallSets, ← forall_and, ← finite_preimage_inl_and_inr,
    preimage_setOf_eq, (· ∘ ·), eventually_and]

Locally Finite Family via Sum Decomposition

Informal description

A family of sets $\{f_i\}_{i \in \iota \oplus \iota'}$ in a topological space $X$ is locally finite if and only if both the subfamilies $\{f_{\text{inl}(i)}\}_{i \in \iota}$ and $\{f_{\text{inr}(i')}\}_{i' \in \iota'}$ are locally finite.

LocallyFinite.sumElim theorem

{g : ι' → Set X} (hf : LocallyFinite f) (hg : LocallyFinite g) : LocallyFinite (Sum.elim f g)

Full source

theorem LocallyFinite.sumElim {g : ι' → Set X} (hf : LocallyFinite f) (hg : LocallyFinite g) :
    LocallyFinite (Sum.elim f g) :=
  locallyFinite_sum.mpr ⟨hf, hg⟩

Locally Finite Family under Sum Combination

Informal description

Let $\{f_i\}_{i \in \iota}$ and $\{g_j\}_{j \in \iota'}$ be two locally finite families of sets in a topological space $X$. Then the combined family $\{h_k\}_{k \in \iota \oplus \iota'}$ defined by $h_{\text{inl}(i)} = f_i$ and $h_{\text{inr}(j)} = g_j$ is also locally finite.

locallyFinite_option theorem

{f : Option ι → Set X} : LocallyFinite f ↔ LocallyFinite (f ∘ some)

Full source

theorem locallyFinite_option {f : Option ι → Set X} :
    LocallyFiniteLocallyFinite f ↔ LocallyFinite (f ∘ some) := by
  rw [← (Equiv.optionEquivSumPUnit.{0, _} ι).symm.locallyFinite_comp_iff, locallyFinite_sum]
  simp only [locallyFinite_of_finite, and_true]
  rfl

Locally Finite Family via Option Decomposition: $\{f_i\}_{i \in \text{Option } \iota}$ is locally finite iff $\{f_{\text{some}(i)}\}_{i \in \iota}$ is locally finite

Informal description

A family of sets $\{f_i\}_{i \in \text{Option } \iota}$ in a topological space $X$ is locally finite if and only if the subfamily $\{f_{\text{some}(i)}\}_{i \in \iota}$ is locally finite.

LocallyFinite.option_elim' theorem

(hf : LocallyFinite f) (s : Set X) : LocallyFinite (Option.elim' s f)

Full source

theorem LocallyFinite.option_elim' (hf : LocallyFinite f) (s : Set X) :
    LocallyFinite (Option.elim' s f) :=
  locallyFinite_option.2 hf

Locally Finite Family via Option Elimination

Informal description

Let $\{f_i\}_{i \in \iota}$ be a locally finite family of sets in a topological space $X$, and let $s \subseteq X$ be a set. Then the family $\{g_i\}_{i \in \text{Option } \iota}$ defined by $g_{\text{some}(i)} = f_i$ and $g_{\text{none}} = s$ is also locally finite.

LocallyFinite.eventually_subset theorem

 {s : ι → Set X} (hs : LocallyFinite s) (hs' : ∀ i, IsClosed (s i)) (x : X) : ∀ᶠ y in 𝓝 x, {i | y ∈ s i} ⊆ {i | x ∈ s i}

Full source

theorem LocallyFinite.eventually_subset {s : ι → Set X}
    (hs : LocallyFinite s) (hs' : ∀ i, IsClosed (s i)) (x : X) :
    ∀ᶠ y in 𝓝 x, {i | y ∈ s i} ⊆ {i | x ∈ s i} := by
  filter_upwards [hs.iInter_compl_mem_nhds hs' x] with y hy i hi
  simp only [mem_iInter, mem_compl_iff] at hy
  exact not_imp_not.mp (hy i) hi

Neighborhood Containment Property for Locally Finite Closed Families

Informal description

Let $\{s_i\}_{i \in \iota}$ be a locally finite family of closed sets in a topological space $X$. For any point $x \in X$, there exists a neighborhood $U$ of $x$ such that for all $y \in U$, the set of indices $\{i \mid y \in s_i\}$ is contained in $\{i \mid x \in s_i\}$.