Theorems · Theorem · general topology

LocallyFinite.eventually_subset

∀ {ι : Type u_1} {X : Type u_4} [inst : TopologicalSpace X] {s : ι → Set X},
  LocallyFinite s → (∀ (i : ι), IsClosed (s i)) → ∀ (x : X), ∀ᶠ (y : X) in nhds x, {i | y ∈ s i} ⊆ {i | x ∈ s i}

Defined in

Mathlib.Topology.LocallyFinite

Cited by

1 results in Mathlib

Foundations

Depth 79 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

TopologicalSpace