English
LocallyFinite f is equivalent to a condition involving small neighborhoods: for every x, the family {f_i ∩ s} has finite nonempty intersections for s in a basis of small sets around x.
Русский
Локально конечна f тогда и только тогда, когда для каждой x существует базис малых окрестностей, в которых {f_i ∩ s} имеет конечное множество непустых пересечений.
LaTeX
$$LocallyFinite f ↔ ∀ x, ∀ᶠ s in (𝓝 x).smallSets, {i | (f i ∩ s).Nonempty}.Finite$$
Lean4
theorem _root_.locallyFinite_iff_smallSets :
LocallyFinite 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
