Theorems · Definition · general topology

LocallyFinite

{ι : Type u_1} → {X : Type u_4} → [TopologicalSpace X] → (ι → Set X) → Prop

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.

Defined in

Mathlib.Topology.LocallyFinite

Cited by

141 results in Mathlib

Foundations

Depth 19 from the axioms, rests on 96 definitions · uses propext, Quot.sound

Assumes

TopologicalSpace