English
If f is locally finite and there is a HasBasis (p,s) at x, there exists i with p(i) and the family {f(j) ∩ s(i)} is finite in the sense of nonempty intersections.
Русский
Пусть f локально конечна и у x есть базис HasBasis (p,s). Существует i с p(i) и множество {j: f(j) ∩ s(i) не пусто} конечно.
LaTeX
$$LocallyFinite f → ∀ {p : ι' → Prop} {s : ι' → Set X} {x : X}, (𝓝 x).HasBasis p s → ∃ i, p i ∧ {j | (f j ∩ s i).Nonempty}.Finite$$
Lean4
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⟩
